summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
Commit message (Expand)AuthorAge
...
* using model instead of labelsGravatar Unknown2012-02-23
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* Boogie: fixed proof-obligation countingGravatar Rustan Leino2012-01-09
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ...Gravatar wuestholz2011-12-02
* Remove invariant that was just wrongGravatar Michal Moskal2011-11-28
* refactoring houdini so that it creates only a single instance of z3Gravatar qadeer2011-11-16
* Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
* partial check in regarding getting states working with stratified inliningGravatar qadeer2011-09-06
* reverting irreducible handling temporarilyGravatar qadeer2011-08-21
|\
* | added code to handle irreducible graphsGravatar qadeer2011-08-20
* | minor refactoringGravatar qadeer2011-08-17
* | deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
* | Added "procedure-copy bounding" for lazy inliningGravatar Unknown2011-08-10
* | further changes for making houdini workGravatar qadeer2011-08-04
|/
* ported all the counterexample code to Michal's new Model class; the goal is t...Gravatar Unknown2011-06-27
* early clearing of live variables and incarnation mapsGravatar qadeer2011-06-24
* implementation of iterative LetVCGravatar qadeer2011-06-23
* Bug fix for trace generation with extractLoop optionGravatar Unknown2011-06-23
* LetVC can get null label2absy from lazy inlining. So, I weakened the precond...Gravatar qadeer2011-05-03
* modified letvc generation so that the use of control flow function and labels...Gravatar qadeer2011-04-15
* added reachability information to the VC and used that to support arbitrary a...Gravatar Unknown2011-04-14
* minor fix with loopy counterexample generationGravatar akashlal2011-03-18
* new algorithm for dead code detection (vc:doomed)Gravatar schaef2011-03-15
* Replaced all dictionaries that mapped to bool (i.e., were being used to imple...Gravatar mikebarnett2011-03-10
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
* Don't treat "Inconclusive" answer as fatal when splitting.Gravatar MichalMoskal2011-02-02
* Add new feature: {:selective_checking} on procedures. See testcase for a desc...Gravatar MichalMoskal2010-12-17
* Add functions generated in lambda-expansion of function body to top-level pro...Gravatar MichalMoskal2010-12-17
* Refactoring: pulled out all code for stratified inlining to a new file.Gravatar akashlal2010-11-23
* Changed stratified inlining: can now be user-guidedGravatar akashlal2010-11-22
* Minor updates for printing coverage graph of stratified inliningGravatar akashlal2010-11-14
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
* Boogie:Gravatar rustanleino2010-10-12
* Minor fix to recursion depth in stratified inlining algorithm.Gravatar akashlal2010-10-02
* Boogie:Gravatar rustanleino2010-09-24
* Boogie:Gravatar rustanleino2010-09-23
* Some simplifications to coverage reporting for StratifiedInlining.Gravatar akashlal2010-09-19
* Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.Gravatar akashlal2010-09-18
* Added more stat printingGravatar akashlal2010-09-16
* Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal tha...Gravatar akashlal2010-09-05
* Fixed a performance issue with StratifiedInliningGravatar akashlal2010-09-05
* Fix for extractLoopsGravatar akashlal2010-09-04
* Henrique's addition to the the ErrorHandler API to retrieve modelsGravatar qadeer2010-09-03
* Bug fix for StratifiedInlining. Use extra Booleans to model procedure calls, ...Gravatar akashlal2010-09-02
* Minor fix to my previous commitGravatar akashlal2010-09-01
* Added a way of recovering counterexample paths after loop extraction. Stable,...Gravatar akashlal2010-09-01
* Boogie: Commented out all occurences of repeated inherited contracts - makes ...Gravatar tabarbe2010-08-27
* bug fixes in z3apiGravatar qadeer2010-08-26