Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | changed behavior of InlinedEnsures so that free ensures is skipped unless an ↵ | 2012-06-01 | |
| | | | | attribute called :assume is there | ||
* | fixed a completeness problem in houdini with inlining | 2011-12-18 | |
| | |||
* | fixed bug in the inlineDepth option for houdini | 2011-11-23 | |
| | | | | small clean up in the inlining implementation | ||
* | changed the semantics of requires and ensures for inlined procedures | 2011-11-17 | |
| | |||
* | changed inlining code so that candidate preconditions and postconditions are ↵ | 2011-11-15 | |
| | | | | ignored | ||
* | added the option /inlineDepth:n. This option defaults to -1. If the user ↵ | 2011-11-13 | |
| | | | | | | provides a non-negative number then that number is used to inline procedures not annotated by {:inline n} attribute. | ||
* | Boogie: Get rid of {:inline} attributes on axioms | 2011-10-27 | |
| | |||
* | Replaced all dictionaries that mapped to bool (i.e., were being used to ↵ | 2011-03-10 | |
| | | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null. | ||
* | Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵ | 2011-03-10 | |
| | | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked. | ||
* | fixed a small bug in inline code | 2010-12-20 | |
| | |||
* | Cleanup up the inlining code | 2010-12-15 | |
| | | | | | 1. For some reason, constructors weren't being inlined. Now they can be. 2. Cleaned up the search for implementations | ||
* | Boogie: Committing changed source files | 2010-08-20 | |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | 2010-08-20 | |