Re: freeboogie: prelude file

[Radu Grigore]

On Tue, Feb 1, 2011 at 8:24 AM, Cristiano Bertolini
<cbert...@gmail.com> wrote:
> I'm trying to generate a bpl file from a java class using freeboogie
> but I'm not able to find the prelude file at svn.

You can generate Boogie from Java using BmlToBpl [1], which generates
a background theory from within its code [2], rather than having a
separate file. Similarly, FreeBoogie generates all the background
needed by Z3 from within its code (but that's almost nothing).

regards,
radu

[1] http://code.google.com/p/freeboogie/source/browse/#svn%2Ftrunk%2FBmlToBpl%253Fstate%253Dclosed
[2] http://code.google.com/p/freeboogie/source/browse/trunk/BmlToBpl/src/b2bpl/translation/Translator.java#470

[Radu Grigore]

On Wed, Feb 2, 2011 at 5:35 AM, Cristiano Bertolini
<cbert...@gmail.com> wrote:
> I'm actually looking for a bpl
> file that provides the procedure definitions for the very basic Java
> methods such as .toString() or .getHashCode().

Those procedure definitions should be generated by BmlToBpl, and they
should definitely *not* be shipped in a bpl file. There is nothing
special about the JRE.

I filed two bugs [1,2] against BmlToBpl. Thanks for reporting.
Unfortunately, there's also a similar problem [3] with abstract
methods. You may star these bug-reports to get news when they are
fixed.

I understand that it must be annoying to write the procedure
definitions by hand.

regards,
radu

[1] http://code.google.com/p/freeboogie/issues/detail?id=70
[2] http://code.google.com/p/freeboogie/issues/detail?id=69
[3] http://code.google.com/p/freeboogie/issues/detail?id=61

[Cristiano Bertolini]

sorry, maybe I was a bit imprecise. I'm actually looking for a bpl

file that provides the procedure definitions for the very basic Java

methods such as .toString() or .getHashCode(). In fact, I do not need
a real specification for those methods but right now, I end up with
errors because of calls to undefined methods.

Thanks,
Cristiano