Strange error message "unhandled macro ignore_me"

Nov 7, 2012 at 4:06 PM

I am getting the following error message from vcc

OOPS: unhandled macro ignore_me
Verification errors in 4 function(s)
Exiting with 3 (1 error(s).)


What does this mean ? I am clueless of what might be wrong in the code at stake.



Nov 7, 2012 at 4:44 PM

I have another strange error :( 

(0,0) : error : undeclared identifier: $bogus
attempting to dump BPL to buggy.bpl
Verification errors in 5 function(s)
Exiting with 3 (1 error(s).)



Nov 7, 2012 at 6:46 PM

Those are bugs in VCC and should not occur. It would help if you have minimal examples that exhibit the behaviour (in which case you could also file bug reports in the tracker), or at the very least if you can share the code that causes the errors (in which case I'll take a long look at it and file a bug report).

Nov 7, 2012 at 6:51 PM
Edited Nov 7, 2012 at 6:52 PM

Well, yes, of course ...  I assume that to be the case (bugs)  :)  ...

I'll try to reproduce it ... but I find it hard ... I have no context information from the vcc output.

Should I pass a special switch to  vcc in order to get more info?


Nov 8, 2012 at 9:30 AM

For the second error, you could try running Boogie on the dump file (you should only need to run "boogie buggy.bpl", without adding the prelude) to identify the faulty piece of Boogie code and get a more interesting error message. Tracing that back to the source is another matter, but just seeing the error message may cause a "Haha!" kind of moment and help you narrow the problem down if you recognize, for example, a variable name

The first error, unfortunately, means that VCC doesn't even get to the stage where Boogie code is output, and as far as I know there is no switch that will be very helpful to you. If you feel adventurous, you can try compiling VCC from source and running it in the Visual Studio debugger to see exactly where it fails (there are also switches that would help identify the transformation pass that fails, but would probably not help with identifying the part of the input that causes the failure). However, the easiest solution is often to remove code until the verification fails properly and recursively zoom in on the faulty sections.

Nov 13, 2012 at 1:36 PM

Here's the output of boogie in relation to the second error message. 

Boogie program verifier version 2.1.40227.0, Copyright (c) 2003-2011, Microsoft.
buggy.bpl(3927,29): Error: undeclared identifier: $bogus
buggy.bpl(3929,28): Error: undeclared identifier: $bogus
2 name resolution errors detected in buggy.bpl

The  boogie code in I reveals at lines 3927/3929:

procedure main#block#0(P#S_ghost_data__: $ptr, P#a: $ptr, addr.rank: $ptr, P#request: $ptr) returns ($result: bool);
  requires $top_writable($s, $bogus, $phys_ptr_cast(P#request, ^Request));
  modifies $s, $cev_pc;
  ensures $top_writable($s, $bogus, $phys_ptr_cast(P#request, ^Request));
  free ensures $writes_nothing(old($s), $s);
  free ensures $call_transition(old($s), $s);



Nov 13, 2012 at 2:27 PM

Without the VCC source, I am afraid there is very little I can do to help, except tell you that VCC is having issues handling the contract you gave to the first block in your main() function. This may help you focus your efforts in isolating a minimal example.

Maybe someone with more experience dealing with VCC internals (and timestamps in particular) can pitch in?


Nov 13, 2012 at 4:43 PM

It was indeed strange ... that's why I have trouble reproducing it with a simple example. 

Meanwhile, I overcomed the problem somehow, by modifying my code.

I have a set of related questions that I'll post in the forum during this week.

Thanks a lot