summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.ssc
Commit message (Expand)AuthorAge
* Boogie\VCGeneration: Renaming sources in preparation for my addition of the p...Gravatar tabarbe2010-07-28
* Boogie: Added interprocedural live variable analysis. Flag to turn it on: "/l...Gravatar akashlal2010-07-19
* /stratifiedInline:n eagerly inlines n times before calling the stratified inl...Gravatar akashlal2010-07-10
* Boogie: Bug fix for stratified inliningGravatar akashlal2010-07-07
* Boogie: Added stratified inlining. It is enabled using the flag /stratifiedIn...Gravatar akashlal2010-07-07
* 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
* (no commit message)Gravatar qadeer2010-02-12
* Support {:PossiblyUnreachable} attribute on assertsGravatar MichalMoskal2009-11-20
* modified the doom checking. It is now able to report only the relevant statem...Gravatar schaef2009-11-18
* * 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
* 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-11-24 09:23:43 +0000