Boogie Options

Mar 31, 2010 at 6:55 PM
I am wondering if anyone can help me configuring Boogie verifier. Is there anyway I can make it ignore array bound checks? I need that for an experiment I am conducting using Spec# and Boogie.
Mar 31, 2010 at 9:53 PM

I think you're referring to SscBoogie, which is the Spec# program verifier (which is built on top of Boogie).  A better forum is probably

Anyway, SscBoogie unfortunately does not have any such options.  (They would be nice to have, so if you would like to make such changes in the code, that would be great.)  I can think of two workarounds.  One workaround is to add Spec# assume statements before array accesses.  For example, before a statement:

x = a[k];

you may add:

assume 0 <= k && k < a.Length;

If your code uses arrays all over the place, this would be tedious.  A different workaround would then be to let SscBoogie produce the warnings, but then for you to ignore them.  Note that you only get 5 warnings per method, so if you get a lot of array bounds warnings, you may want to use the /errorLimit flag to ask for more warnings.