Parsing of pragmas in comments?

Nov 27, 2009 at 2:49 PM

Hi all,

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

  For example, the following BPL

/*
#unrecognized
*/

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

Coordinator
Nov 30, 2009 at 8: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?

Thanks,
  Rustan

Dec 15, 2009 at 8:52 AM

Hi Rustan,

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

Best regards, Mark