如何在使用Mono編譯時引用Microsoft.Boogie？

using System; 
using System.Collections.Generic; 
using Microsoft.Boogie; 

public class Trace 
{ 
    public static void Main(string[] args) 
{ 
    if (args.Length != 2){ 
     return; 
    } 
    Program program = new Program(); 
    List<string> defines = new List<string>(); 
    Parser.Parse(args[0], defines, out program); 

    string[] lines = System.IO.File.ReadAllLines(args[1]); 
    Dictionary< Block, List<Block> > adj = new Dictionary< Block, List<Block> >(); 

    foreach (Declaration D in program.TopLevelDeclarations){ 
     Implementation I = D as Implementation; 
     if(I != null){ 
      foreach (Block B in I.Blocks){ 
       object cmd = B.TransferCmd; 
       if(cmd is GotoCmd){ 
        List<Block> target = cmd.labelTargets; 
        adj.insert(B, target); 
       } 
       else if(cmd is ReturnCmd){ 
        adj.insert(B, null); 
       } 
      } 
     } 
    } 
} 
}

我是C＃的新手，我被卡在如何遍歷program.TopLevelDeclarations。如何在使用Mono編譯時引用Microsoft.Boogie？

試圖迭代一個簡單的列表，但當我嘗試包括Microsoft Boogie庫時，編譯器會拋出一些錯誤。

我編譯在Ubuntu 13.04使用gmcs使用命令我的程序：

gmcs -r:../../boogie/Binaries/Boogie.exe -r:../../boogie/Binaries/Core.dll Trace.cs

其中給出了以下錯誤：

Missing method .ctor in assembly /home/boogie/Binaries/Core.dll, type System.Diagnostics.Contracts.ContractClassAttribute

Can`t find custom attr constructor image: /home/boogie/Binaries/Core.dll mtoken: 0x0a000463

Trace.cs(19,52): error CS0584: Internal compiler error: Could not load type System.Diagnostics.Contracts.ContractClassAttribute from assembly Core .

Trace.cs(19,36): error CS0266: Cannot implicitly convert type object to System.Collections.Generic.List<Microsoft.Boogie.Declaration> . An explicit conversion exists (are you missing a cast?)

Trace.cs(22,30): error CS0584: Internal compiler error: Could not import type Microsoft.Boogie.Implementation from Core, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16

Trace.cs(22,30): error CS0266: Cannot implicitly convert type object to bool . An explicit conversion exists (are you missing a cast?)

Trace.cs(23,55): error CS0584: Internal compiler error: Could not import type Microsoft.Boogie.Implementation from Core, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16

Trace.cs(23,33): error CS1579: foreach statement cannot operate on variables of type object because it does not contain a definition for GetEnumerator or is inaccessible

Compilation failed: 6 error(s), 0 warnings

有誰知道如何解決這一問題？我是否錯誤地包括了圖書館？

來源

2013-12-08 anirudh

機器上的庫是否存在？你在使用Mono框架嗎？另外，如果你在Ubuntu上，你可以使用[MonoDevelop]（http://monodevelop.com/Download）而不是手動編譯，這將爲你解決大部分這些問題。 – valverij

是的，我正在使用MonoDevelop – anirudh

我似乎無法找到的Microsoft.Boogie.Declaration源，但考慮到錯誤消息它具有[ContractClass]屬性，其中編譯器找不到：

Trace.cs(19,52): error CS0584: Internal compiler error: Could not load type 'System.Diagnostics.Contracts.ContractClassAttribute' from assembly 'Core'.

由於這種類型Microsoft.Boogie.Declaration無法加載的，導致program.TopLevelDeclarations的List<Declaration>明顯被「stubbed」爲某種object。這反過來導致您的代碼失敗，因爲您無法遍歷對象。

在.NET 4中，ContractClassAttribute被添加到mscorlib。您正在使用gmcs，根據mono's CSharp Compiler manual page編譯的是.NET 2.0。

我想你最好使用mcs進行編譯，這在那裏推薦。

來源

2013-12-08 12:22:28 CodeCaster

如何在使用Mono編譯時引用Microsoft.Boogie？

回答

相關問題