summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| * | Remove invariant that was just wrongGravatar Michal Moskal2011-11-28
| * | MergeGravatar akashlal2011-11-26
| |\ \
| * | | Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
| | * | Boogie build succeededGravatar CodeplexBot2011-11-25
| |/ / |/| |
* | | MergeGravatar qadeer2011-11-24
|\| |
* | | added some more statistics to houdiniGravatar qadeer2011-11-24
| * | minor bug fix in SIGravatar akashlal2011-11-24
| * | minor changes to summary computationGravatar akashlal2011-11-24
|/ /
* | fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
* | MergeGravatar qadeer2011-11-22
|\ \
* | | augmented the worklist with an explicit attached setGravatar qadeer2011-11-22
| * | Boogie build succeededGravatar CodeplexBot2011-11-23
| | * MergeGravatar Rustan Leino2011-11-22
| | |\ | | |/ | |/|
| * | MergeGravatar Rustan Leino2011-11-22
| |\ \ | |/ / |/| |
| * | DafnyExtension: fix up compilation (once again)Gravatar Rustan Leino2011-11-22
| * | Dafny: call C# compiler directly from inside Dafny, and optionally produce a ...Gravatar Rustan Leino2011-11-22
* | | MergeGravatar qadeer2011-11-22
|\| |
| * | Boogie: don't resolve ignored types (that is, "extern" types that have been t...Gravatar Rustan Leino2011-11-22
* | | MergeGravatar qadeer2011-11-22
|\| |
* | | added support for handling duplicate axiomsGravatar qadeer2011-11-22
| * | fixes to summary computationGravatar Unknown2011-11-22
| | * Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbi...Gravatar Rustan Leino2011-11-21
| * | Refactored translator so it can be called programmatically and return theGravatar Mike Barnett2011-11-21
|/ /
* | Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2011-11-21
|\ \
| * | BCT: Initialize Boogie's command-line options object correctly before usingGravatar Mike Barnett2011-11-21
* | | MergeGravatar Unknown2011-11-21
|\ \ \
* | | | Generating useful, and guarateed by construction, postconditions and loop inv...Gravatar Unknown2011-11-21
| * | | Boogie build succeededGravatar CodeplexBot2011-11-21
| * | | Added lazy summary computation to stratified inlining (not finished yet)Gravatar akashlal2011-11-20
| |/ /
| * | commented calls to GC.Collect()Gravatar qadeer2011-11-18
| * | changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
| * | Boogie build succeededGravatar CodeplexBot2011-11-17
| |/
| * MergeGravatar Rustan Leino2011-11-16
| |\
| * | Dafny: fixed bad Code ContractsGravatar Rustan Leino2011-11-16
| | * Boogie build failedGravatar CodeplexBot2011-11-17
| |/
| * MergeGravatar qadeer2011-11-16
| |\
| * | /contractInfer always prints the computed assignment nowGravatar qadeer2011-11-16
| * | refactoring houdini so that it creates only a single instance of z3Gravatar qadeer2011-11-16
| | * Translate AddressOf expressions correctly.Gravatar Mike Barnett2011-11-16
| | * Boogie: fixed build error (incorrect type in Contract.Result)Gravatar Rustan Leino2011-11-16
| * | Eliminated unused argument in the constructor for CheckerGravatar qadeer2011-11-16
| | * Tagging EMIC CC.NET build 2.1.31116.0Gravatar VccBuildServer2011-11-16
| | * MergeGravatar Michal Moskal2011-11-16
| | |\ | |_|/ |/| |
| * | MergeGravatar qadeer2011-11-16
| |\ \ | |/ / |/| |
| * | simple fix in houdiniGravatar qadeer2011-11-16
* | | MergeGravatar Unknown2011-11-16
|\ \ \
* | | | Small fix.Gravatar Unknown2011-11-16
| * | | Load all assemblies before doing anything else so that the unification forGravatar Mike Barnett2011-11-16
|/ / /
* | | MergeGravatar Unknown2011-11-16
|\ \ \
* | | | Better support for race-checking contractsGravatar Unknown2011-11-16