summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
Commit message (Expand)AuthorAge
* 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
* fixed z3api so that it works on small examples now.Gravatar qadeer2010-08-24
* Added user option for bounding inlining depthGravatar akashlal2010-08-20
* Added recursion-bound-guided search for stratified inliningGravatar akashlal2010-08-19
* Some reformatting and refactoringGravatar akashlal2010-08-18
* Added option for displaying stratified inlining's searchGravatar akashlal2010-08-18
* Stratified inlining: Changed recursion into a loop.Gravatar akashlal2010-08-16
* Bug fix for stratified inlining trace generationGravatar akashlal2010-08-16
* Added more options for stratified inliningGravatar akashlal2010-08-16
* Added the option /extractLoops to extract loops as procedure calls. If eithe...Gravatar qadeer2010-08-11
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* More line ending fixups.Gravatar MichalMoskal2010-08-06
* Commiting Michal's fix for VCGravatar stobies2010-08-05
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
* Boogie: VCGeneration port part 1/3: Replacing old source files with ported ve...Gravatar tabarbe2010-07-28
* Boogie\VCGeneration: Renaming sources in preparation for my addition of the p...Gravatar tabarbe2010-07-28