summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* VCC: Fixes for recent prelude changesGravatar Michal Moskal2011-12-02
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ...Gravatar wuestholz2011-12-02
* added a mechanism for supplying the list of input bpl files inside a .txt fileGravatar qadeer2011-12-01
* a bug fix in model parsingGravatar qadeer2011-11-30
* MergeGravatar qadeer2011-11-28
|\
* | fixed a bug in model parsingGravatar qadeer2011-11-28
| * 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
* | 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
| * MergeGravatar 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
|/
* MergeGravatar Unknown2011-11-21
|\
* | Generating useful, and guarateed by construction, postconditions and loop inv...Gravatar Unknown2011-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
| * Dafny: fixed bad Code ContractsGravatar Rustan Leino2011-11-16
| * 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
| | * 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
| | * MergeGravatar Michal Moskal2011-11-16
| | |\ | |_|/ |/| |
| * | MergeGravatar qadeer2011-11-16
| |\ \ | |/ / |/| |
| * | simple fix in houdiniGravatar qadeer2011-11-16
* | | Small fix.Gravatar Unknown2011-11-16
* | | MergeGravatar Unknown2011-11-16
|\ \ \
* | | | Better support for race-checking contractsGravatar Unknown2011-11-16
| * | | MergeGravatar akashlal2011-11-16
| |\ \ \
| | * | | Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
| | |/ /
| | | * 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 CommandLine...Gravatar Rustan Leino2011-11-15
| | | * VCC: Recognize $resultGravatar Michal Moskal2011-11-15
| | |/
| * | MergeGravatar Rustan Leino2011-11-15
| |\|
| | * MergeGravatar qadeer2011-11-15
| | |\ | |_|/ |/| |