Boogie

Feb 21, 2013 at 2:48 PM
Hi All,

We know that Boogie can locate the failure assertions by returning the line number, but how to find the failure assertion node in the BoogieAST tree ?

Thanks!
Nightrise
Coordinator
Feb 23, 2013 at 3:47 AM
A pointer to the AST node for the assert, requires, or ensures sits inside the Counterexample object. See method ProcessOutcome in BoogieDriver.cs, for example. If the Counterexample is an AssertCounterexample, you'll find the AssertCmd in the .FailingAssert field, and so on.

Rustan
Feb 23, 2013 at 5:14 AM
Hi Rustan,

It helps a lot, thank you!

Nightrise