Parsing of pragmas in comments?

Nov 27, 2009 at 3:49 PM

Hi all,

  Boogie seems to scan for pragmas in multi-line /* ... */ comments -- is this intentional?

  For example, the following BPL


results in

Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
intentional.bpl(2,0): Error: Unrecognized pragma: #unrecognized
1 parse errors detected in intentional.bpl

Best, Mark

Nov 30, 2009 at 9:50 PM

Hi Mark,

I don't remember any particular reason for this.  Perhaps it was easier to do in the implementation?  The current behavior differs from the behavior of the C pre-processor, so I agree this is a bug.  Can you fix it?


Dec 15, 2009 at 9:52 AM

Hi Rustan,

  thanks for the info!  I'll look into it, but this will probably take a while...

Best regards, Mark