Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | fixed bug in the inlineDepth option for houdini | 2011-11-23 | |
| | | | | small clean up in the inlining implementation | ||
* | Merge | 2011-11-22 | |
|\ | |||
* | | augmented the worklist with an explicit attached set | 2011-11-22 | |
| | | |||
| * | Boogie build succeeded | 2011-11-23 | |
| | | |||
| * | Merge | 2011-11-22 | |
| |\ | |/ |/| | |||
| * | DafnyExtension: fix up compilation (once again) | 2011-11-22 | |
| | | |||
| * | Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵ | 2011-11-22 | |
| | | | | | | | | .cs file with the new /spillTargetCode switch | ||
* | | Merge | 2011-11-22 | |
|\| | |||
| * | Boogie: don't resolve ignored types (that is, "extern" types that have been ↵ | 2011-11-22 | |
| | | | | | | | | thrown out) | ||
* | | Merge | 2011-11-22 | |
|\| | |||
* | | added support for handling duplicate axioms | 2011-11-22 | |
| | | |||
| * | fixes to summary computation | 2011-11-22 | |
| | | |||
| * | Refactored translator so it can be called programmatically and return the | 2011-11-21 | |
|/ | | | | translated program in memory without writing it to disk. | ||
* | Automated merge with https://hg01.codeplex.com/boogie | 2011-11-21 | |
|\ | |||
| * | BCT: Initialize Boogie's command-line options object correctly before using | 2011-11-21 | |
| | | | | | | | | Boogie. | ||
* | | Merge | 2011-11-21 | |
|\ \ | |||
* | | | Generating useful, and guarateed by construction, postconditions and loop ↵ | 2011-11-21 | |
| | | | | | | | | | | | | invariants for kenrel procedures. | ||
| * | | Boogie build succeeded | 2011-11-21 | |
| | | | |||
| * | | Added lazy summary computation to stratified inlining (not finished yet) | 2011-11-20 | |
| |/ | |||
| * | commented calls to GC.Collect() | 2011-11-18 | |
| | | |||
| * | changed the semantics of requires and ensures for inlined procedures | 2011-11-17 | |
| | | |||
| * | Boogie build succeeded | 2011-11-17 | |
| | | |||
| * | Merge | 2011-11-16 | |
| |\ | |||
| * | | Dafny: fixed bad Code Contracts | 2011-11-16 | |
| | | | |||
| | * | Boogie build failed | 2011-11-17 | |
| |/ | |||
| * | Merge | 2011-11-16 | |
| |\ | |||
| * | | /contractInfer always prints the computed assignment now | 2011-11-16 | |
| | | | | | | | | | | | | enabled the houdini regressions | ||
| * | | refactoring houdini so that it creates only a single instance of z3 | 2011-11-16 | |
| | | | |||
| | * | Translate AddressOf expressions correctly. | 2011-11-16 | |
| | | | | | | | | | | | | Fixes for problems when translating generic type parameters. | ||
| | * | Boogie: fixed build error (incorrect type in Contract.Result) | 2011-11-16 | |
| | | | |||
| * | | Eliminated unused argument in the constructor for Checker | 2011-11-16 | |
| | | | |||
| | * | Tagging EMIC CC.NET build 2.1.31116.0 | 2011-11-16 | |
| | | | |||
| | * | Merge | 2011-11-16 | |
| | |\ | |_|/ |/| | | |||
| * | | Merge | 2011-11-16 | |
| |\ \ | |/ / |/| | | |||
| * | | simple fix in houdini | 2011-11-16 | |
| | | | |||
* | | | Merge | 2011-11-16 | |
|\ \ \ | |||
* | | | | Small fix. | 2011-11-16 | |
| | | | | |||
| * | | | Load all assemblies before doing anything else so that the unification for | 2011-11-16 | |
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | the Core Assembly identity can happen correctly. Cache things in the sink based on the mangled name rather than the interned key: this prevents clashes in the Boogie program, but might mask some errors due to different types/members with the same full name (minus the assembly name of course). Translate generic parameters as Ref instead of Box if they are constrained to be a reference or struct (since we translate structs as Ref). [Experimental] | ||
* | | | Merge | 2011-11-16 | |
|\ \ \ | |||
* | | | | Better support for race-checking contracts | 2011-11-16 | |
| | | | | |||
| * | | | Boogie build failed | 2011-11-16 | |
| | | | | |||
| * | | | Merge | 2011-11-16 | |
| |\ \ \ | |||
| | * | | | Debugging output for stratified inlining. Emit attribute on Ensures while | 2011-11-16 | |
| | |/ / | | | | | | | | | | | | | printing it. | ||
| | | * | BVD: Fix display bug | 2011-11-15 | |
| | | | | |||
| | | * | VCC: Further data type improvements | 2011-11-15 | |
| | | | | |||
| | | * | VCC: Better display of data type values | 2011-11-15 | |
| | | | | |||
| * | | | DafnyExtension: fixed build problems | 2011-11-15 | |
| | | | | |||
| * | | | Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵ | 2011-11-15 | |
| | | | | | | | | | | | | | | | | CommandLineOptions to separate the options that belong to these 3 tools. | ||
| | | * | VCC: Recognize $result | 2011-11-15 | |
| | |/ | |||
| * | | Merge | 2011-11-15 | |
| |\| |