summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Expand)AuthorAge
...
* Boogie: Added stratified inlining. It is enabled using the flag /stratifiedIn...Gravatar akashlal2010-07-07
* Improved error messages for doomed program points.Gravatar schaef2010-06-15
* Added another option for lazy inlining based on macro expansion. This option...Gravatar qadeer2010-05-03
* 1. Fixed lazy inlining implementation so that inlined procedures use live var...Gravatar qadeer2010-04-30
* 1. couple of bug fixes in interprocedural error trace generationGravatar qadeer2010-04-23
* Added callee args information to calleeCounterexamplesGravatar qadeer2010-04-21
* Fixed bug in interprocedural counterexample generationGravatar qadeer2010-04-19
* First cut of lazy inlining. The option can be turned on by the flag /lazyInl...Gravatar qadeer2010-04-17
* Dafny: Added definedness checks for all statements (previously, some were mi...Gravatar rustanleino2010-03-13
* Call program-wide lambda desugaring on axioms only. Call it on procedures in ...Gravatar MichalMoskal2010-03-12
* Boogie:Gravatar rustanleino2010-02-20
* 1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linea...Gravatar qadeer2010-02-16
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
* 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-19 07:35:07 +0000