summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
| | | | small clean up in the inlining implementation
* 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
| |\ | |/ |/|
| * 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
| | | | | | | | .cs file with the new /spillTargetCode switch
* | MergeGravatar qadeer2011-11-22
|\|
| * Boogie: don't resolve ignored types (that is, "extern" types that have been ↵Gravatar Rustan Leino2011-11-22
| | | | | | | | thrown out)
* | MergeGravatar qadeer2011-11-22
|\|
* | added support for handling duplicate axiomsGravatar qadeer2011-11-22
| |
| * fixes to summary computationGravatar Unknown2011-11-22
| |
| * Refactored translator so it can be called programmatically and return theGravatar Mike Barnett2011-11-21
|/ | | | translated program in memory without writing it to disk.
* 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
| | | | | | | | Boogie.
* | MergeGravatar Unknown2011-11-21
|\ \
* | | Generating useful, and guarateed by construction, postconditions and loop ↵Gravatar Unknown2011-11-21
| | | | | | | | | | | | invariants for kenrel procedures.
| * | 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
| | | | | | | | | | | | enabled the houdini regressions
| * | refactoring houdini so that it creates only a single instance of z3Gravatar qadeer2011-11-16
| | |
| | * Translate AddressOf expressions correctly.Gravatar Mike Barnett2011-11-16
| | | | | | | | | | | | Fixes for problems when translating generic type parameters.
| | * 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
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | 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]
* | | MergeGravatar Unknown2011-11-16
|\ \ \
* | | | Better support for race-checking contractsGravatar Unknown2011-11-16
| | | |
| * | | Boogie build failedGravatar CodeplexBot2011-11-16
| | | |
| * | | MergeGravatar akashlal2011-11-16
| |\ \ \
| | * | | Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
| | |/ / | | | | | | | | | | | | printing it.
| | | * BVD: Fix display bugGravatar Michal Moskal2011-11-15
| | | |
| | | * VCC: Further data type improvementsGravatar Michal Moskal2011-11-15
| | | |
| | | * VCC: Better display of data type valuesGravatar Michal Moskal2011-11-15
| | | |
| * | | DafnyExtension: fixed build problemsGravatar Rustan Leino2011-11-15
| | | |
| * | | Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵Gravatar Rustan Leino2011-11-15
| | | | | | | | | | | | | | | | CommandLineOptions to separate the options that belong to these 3 tools.
| | | * VCC: Recognize $resultGravatar Michal Moskal2011-11-15
| | |/
| * | MergeGravatar Rustan Leino2011-11-15
| |\|