c# - 用Mono编译时如何引用Microsoft.Boogie？

Question

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 很困惑.

尝试遍历一个简单的列表是可行的，但是当我尝试包含 Microsoft Boogie 时库，编译器会抛出一些错误。

我正在使用 gmcs 编译我的程序在 Ubuntu 13.04 上使用命令:

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

有人知道怎么解决吗？我是否错误地包含了库？

Answer 1

我似乎找不到 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无法加载，导致 List<Declaration>的 program.TopLevelDeclarations显然被某种形式的“ stub ”作为object .这反过来会导致您的代码失败，因为您无法迭代一个对象。

ContractClassAttribute 已添加到 mscorlib在 .NET 4 中。您正在使用 gmcs , 根据mono's CSharp Compiler manual page针对 .NET 2.0 进行编译。

我认为您最好使用 mcs 进行编译，那里推荐。