Boogie Problem

Jan 25, 2013 at 4:51 PM


In Boogie source code, in  BoogieDriver.cs there is a line of code

foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

when I was debugging a file t2.bpl,  impl is 'foo', but why impl.Proc is null ? 


Jan 27, 2013 at 6:08 PM

What I am understanding is that impl stands for the procedure in program, in fact,  when I am debuging the file "t2.bp2", the procedure name in this file is 'foo'

and impl is 'foo', but why impl.Proc is null ? Does not impl.Proc also means the procedure of the program ?  

Thanks for any suggestion...

Jan 27, 2013 at 10:21 PM

I just find the problem, now impl.Proc has the procedure's name. But it comes an Exception which I am very confused

 public override void Typecheck(TypecheckingContext tc) {     //Contract.Requires(tc != null);      Contract.Ensures(Type != null);  // This body is added only because C# insists on it.  It should really be left out, as if TypeCheck still were abstract.      // The reason for mentioning the method here at all is to give TypeCheck a postcondition for all expressions.      {   Contract.Assert(false);        throw new cce.UnreachableException();      }    } 

the last line of code "throw new cce.UnreachableException()"  caused an   unreachableException, an exception of type'cce.UnreachableException' occurred in Core.dll

Does anyone have met this problem before ?


Jan 30, 2013 at 8:04 PM

The Proc field is filled in during resolution.  If you find that it is null, it means you're looking at the AST before it has been resolved (or that the resolution produced some errors).

Usually, the Unreachable exceptions are thrown where there's an unexpected type.  Look (in the debugger) at if statements around it to see what the dynamic type of the expression/statement/declaration you're dealing with is.