summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Expand)AuthorAge
* Boogie: Peephole optimization to reduce depth of formulas created during VC ...Gravatar rustanleino2010-02-15
* (no commit message)Gravatar qadeer2010-02-12
* bugfixGravatar schaef2010-01-28
* Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebu...Gravatar schaef2010-01-28
* Doomed checking now uses the counterexample trace to minimize the number of t...Gravatar schaef2009-12-18
* Added code to (once again) print out prover warnings (under the /proverWarnin...Gravatar rustanleino2009-11-26
* (no commit message)Gravatar schaef2009-11-20
* Support {:PossiblyUnreachable} attribute on assertsGravatar MichalMoskal2009-11-20
* doomed stuff: minor bug fixes / improved output / more test casesGravatar schaef2009-11-19
* modified the doom checking. It is now able to report only the relevant statem...Gravatar schaef2009-11-18
* Fixes crash when modifies set includes a variable twice.Gravatar mkawa2009-11-07
* vc:doomed does not use the console anymore to report resultsGravatar schaef2009-11-02
* Optimized the number of Z3 queries in doomed program point detection.Gravatar schaef2009-09-25
* * Boogie and Dafny: added /cev:<file> optionGravatar rustanleino2009-09-15
* Dafny:Gravatar rustanleino2009-09-14
* Report prover warnings during smoke test via the VerifierCallbackGravatar stobies2009-09-07
* Use callback mechanism to report prover warnings; do not just write them to s...Gravatar stobies2009-09-07
* Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other bit...Gravatar stobies2009-09-07
* Sign assembliesGravatar stobies2009-08-17
* Fixed bug where the remove-empty-blocks optimization had not updated the star...Gravatar rustanleino2009-08-13
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 23:28:20 +0000