search

delcypher / freeboogie

Automatically exported from code.google.com/p/freeboogie
0 stars 1 forks source link

fetch specifications of Java methods that are used #69

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
If method m is called from one of the processed classes, then its contract must 
be in the generated Boogie.

For example, if String methods are used, the user should not need to 
specifically mention java.lang.String as a class to process, because we only 
want the specs, not the implementations.

Original issue reported on code.google.com by radugrig...@gmail.com on 2 Feb 2011 at 5:11