summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/StratifiedVC.cs
Commit message (Expand)AuthorAge
* Minor additions to VC genGravatar Akash Lal2015-07-20
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* Fix for SI: initialize extraRecBoundGravatar Akash Lal2015-06-05
* Simplified StratifiedVC interfaceGravatar akashlal2015-06-01
* Allow for extra instrumentation on program before vc genGravatar Akash Lal2015-05-25
* Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
* Fix for secureVCGenGravatar Akash Lal2015-05-07
* VC gen for security propertiesGravatar akashlal2015-04-05
* Compute MustReach information lazily, on-demandGravatar akashlal2015-03-16
* Added MustReach information to VC genGravatar akashlal2015-03-11
* Handle timeout in refinement loopGravatar akashlal2015-01-28
* SI: print if a bound was reached.Gravatar akashlal2014-10-29
* Minor correctionsGravatar akashlal2014-10-01
* SI: VC gen with labelsGravatar akashlal2014-09-29
* Cleanup: removed unused codeGravatar akashlal2014-09-29
* Fix to VC genGravatar akashlal2014-09-28
* Fix for boolVC generationGravatar akashlal2014-09-27
* Lets have a setter for TopLevelDeclarations as wellGravatar akashlal2014-09-25
* minor fixGravatar akashlal2014-09-24
* Simple VC generation for SIGravatar akashlal2014-09-24
* Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
* Did some refactoring.Gravatar wuestholz2014-09-23
* Bug fix in SIGravatar akashlal2014-08-03
* Some simplificationsGravatar akashlal2014-07-28
* OnModel now carries the result of the prover callGravatar akashlal2014-06-28
* Fix in SI while dealing with timeoutsGravatar akashlal2014-06-27
* keep some stats for debuggingGravatar akashlal2014-05-15
* Added stack boundingGravatar akashlal2014-05-10
* Recursive walking of Exprs doesn't play nice when the depth of the AST is high.Gravatar akashlal2014-01-07
* code cleanupGravatar akashlal2013-11-02
* And a test caseGravatar akashlal2013-10-21
* Bug fix in stratified inlining (triggered by {:inline} functions)Gravatar akashlal2013-10-21
* MergeGravatar Pantazis Deligiannis2013-10-09
|\
* | changes to support a configured errorLimitGravatar Pantazis Deligiannis2013-09-30
| * refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of Genera...Gravatar qadeer2013-09-09
| * Factored out the closure for codeexpr conversion so that it can be reused.Gravatar qadeer2013-09-04
|/
* Fixed several build errors in the 'Checked' configuration.Gravatar wuestholz2013-08-05
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
* BlockSeq: farewellGravatar Ally Donaldson2013-07-22
* CmdSeq: farewellGravatar Ally Donaldson2013-07-22
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
* mergeGravatar Pantazis Deligiannis2013-07-22
|\
| * Large refactoring of Hashtable to Dictionary.Gravatar Ally Donaldson2013-07-22
| * Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a plai...Gravatar Ally Donaldson2013-07-22
* | mergeGravatar Pantazis Deligiannis2013-07-06
|\|
| * Did some refactoring in the execution engine and worked on the parallelization.Gravatar wuestholz2013-07-01
* | merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more compa...Gravatar pantazis2013-06-13
|/
* Parse integers returned by Z3 into BigNumGravatar akashlal2013-01-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 20:13:04 +0000