summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
Commit message (Expand)AuthorAge
...
* z3 process is killed nowGravatar qadeer2012-05-01
* clean up in stratified inliningGravatar qadeer2012-04-29
* eliminated class ErrorModelGravatar qadeer2012-04-28
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* fixed problems with datatypesGravatar qadeer2011-12-29
* Make set iteration order deterministicGravatar Michal Moskal2011-12-07
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ...Gravatar wuestholz2011-12-02
* refactoring houdini so that it creates only a single instance of z3Gravatar qadeer2011-11-16
* Eliminated unused argument in the constructor for CheckerGravatar qadeer2011-11-16
* Name the constant used in @MV_state function applications - otherwise we get ...Gravatar Michal Moskal2011-09-26
* fixes to model value generation for stratified inliningGravatar qadeer2011-09-12
* further fixesGravatar qadeer2011-09-08
* partial check in regarding getting states working with stratified inliningGravatar qadeer2011-09-06
* added code to handle irreducible graphsGravatar qadeer2011-08-20
* 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
* Print recorded value of any typeGravatar akashlal2011-03-21
* Print out requested values in the counterexample traceGravatar akashlal2011-03-17
* 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
* Stratified inlining: Added concrete values to error traces. Added an extra fl...Gravatar akashlal2011-02-17
* Boogie: Did some minor refactoring.Gravatar wuestholz2010-12-10
* Construct @MV_state function only once so it doesn't get renamed to @MV_state...Gravatar MichalMoskal2010-12-02
* Refactoring: pulled out all code for stratified inlining to a new file.Gravatar akashlal2010-11-23
* Dafny: a partial first crack at a Dafny model-viewer provider, including capt...Gravatar rustanleino2010-11-01
* Skip unchagned variables in model dumps. Fix testcaseGravatar MichalMoskal2010-10-14
* Add interfaces for langauge providers. Start with VCC provider.Gravatar MichalMoskal2010-10-12
* Add missing Clone() when storing incarnation maps; update testcase to make th...Gravatar MichalMoskal2010-10-12
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
* Boogie:Gravatar rustanleino2010-10-12
* Boogie: fixed a Code Contract in the sourceGravatar rustanleino2010-10-09
* Add state sequence API and creation, still untestedGravatar MichalMoskal2010-10-08
* Boogie:Gravatar rustanleino2010-09-24
* Boogie:Gravatar rustanleino2010-09-23
* Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal tha...Gravatar akashlal2010-09-05
* Henrique's addition to the the ErrorHandler API to retrieve modelsGravatar qadeer2010-09-03
* 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
* Boogie: Removed some errors with code contracts (commenting out doubly-inheri...Gravatar tabarbe2010-08-27
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* More line ending fixups.Gravatar MichalMoskal2010-08-06
* 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