summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Expand)AuthorAge
* ported all the counterexample code to Michal's new Model class; the goal is t...Gravatar Unknown2011-06-27
* Fixed non-incremental option of stratified inliningGravatar Unknown2011-06-27
* FindLeastToVerify: accept multiple proceduresGravatar Unknown2011-06-26
* Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
* 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
* Add a string for an uninterpreted value in errModelGravatar Unknown2011-06-06
* 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
* mergeGravatar Unknown2011-04-14
|\
* | added reachability information to the VC and used that to support arbitrary a...Gravatar Unknown2011-04-14
| * Stratified Inlining: minor bux fix with recording model valuesGravatar Unknown2011-04-14
|/
* Minor fixesGravatar schaef2011-03-27
* Boogie: fixed contract violation in stratified inliningGravatar rustanleino2011-03-23
* Print recorded value of any typeGravatar akashlal2011-03-21
* Bug fix with model generation.Gravatar akashlal2011-03-21
* minor fix with loopy counterexample generationGravatar akashlal2011-03-18
* Print out requested values in the counterexample traceGravatar akashlal2011-03-17
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
* new algorithm for dead code detection (vc:doomed)Gravatar schaef2011-03-15
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
* 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
* Updated PrepareBoogieZip.bat to include BVD and smt2Gravatar rustanleino2011-03-10
* Added a new solution configuration, Checked, that builds the Checked configur...Gravatar mikebarnett2011-03-07
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
* Handle as-array[...] model elementsGravatar MichalMoskal2011-02-23
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
* Throw exceptions when push/pop interface is used but not implementedGravatar MichalMoskal2011-02-23
* Implement Push/Pop interface.Gravatar MichalMoskal2011-02-23
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21
* Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3Gravatar MichalMoskal2011-02-18
* Kill {:prover "..."} attribute support; no one ever used this stuffGravatar MichalMoskal2011-02-17
* Stratified inlining: Added concrete values to error traces. Added an extra fl...Gravatar akashlal2011-02-17
* Fix with timeoutGravatar akashlal2011-02-12
* Better support for timeoutGravatar akashlal2011-02-12
* Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP prove...Gravatar MichalMoskal2011-02-11
* Minor change to stratified inliningGravatar akashlal2011-02-11
* Added a new method StratifiedVC for refinement.Gravatar akashlal2011-02-08
* implemented /UseUnsatCoreForInlining option for use in stratified inliningGravatar qadeer2011-02-06
* deleted debugging statementGravatar akashlal2011-02-05
* Fix to counterexample generation for over-approx queryGravatar akashlal2011-02-05
* Don't treat "Inconclusive" answer as fatal when splitting.Gravatar MichalMoskal2011-02-02
* stratified inlining: minor fix to the call tree being savedGravatar akashlal2010-12-21
* stratified inlining: record the name of the main procedure.Gravatar akashlal2010-12-18
* 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
* stratified inlining: minor changes to coverage reporterGravatar akashlal2010-12-13
* Boogie: Did some minor refactoring.Gravatar wuestholz2010-12-10