summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Collapse)AuthorAge
...
* | Fixed minor issue.Gravatar wuestholz2014-11-02
| |
* | Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-11-02
| |
* | Did some refactoring.Gravatar wuestholz2014-11-02
| |
* | SI: print if a bound was reached.Gravatar akashlal2014-10-29
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-10-19
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-10-19
| |
* | Did some refactoring.Gravatar wuestholz2014-10-18
| |
* | Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-10-18
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-10-17
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-10-17
| |
* | Did some refactoring.Gravatar wuestholz2014-10-16
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-10-16
| |
* | Fix issue in verification result caching.Gravatar wuestholz2014-10-15
| |
* | Fix issue in verification result caching.Gravatar wuestholz2014-10-15
| |
* | Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-10-14
| |
* | Fix issue in verification result caching for assertions without subsumption.Gravatar wuestholz2014-10-13
| |
* | Add a todo.Gravatar wuestholz2014-10-13
| |
| * Merge FixpointVC changes with mainlineGravatar Ken McMillan2014-10-08
|/|
| * Added "extra recursion bound" to FixedpointVC to support Corral.Gravatar Ken McMillan2014-10-08
| |
* | MergeGravatar akashlal2014-10-01
|\ \
| * | Minor correctionsGravatar akashlal2014-10-01
| | |
* | | fixed StackOverflow in TraceCounterexample;Gravatar qadeer2014-09-30
|/ / | | | | | | converted tail recursion into a loop
* | 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
| |
* | (Subhajit) Added an interface for InterpolatingTheoremProverGravatar akashlal2014-09-24
| |
* | minor fixGravatar akashlal2014-09-24
| |
* | Simple VC generation for SIGravatar akashlal2014-09-24
| |
* | Fixed assertion violation.Gravatar wuestholz2014-09-23
| |
* | Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
| |
* | Did more refactoring.Gravatar wuestholz2014-09-23
| |
* | Did some refactoring.Gravatar wuestholz2014-09-23
| |
* | Fixed an issue in the verification result caching (recycled errors).Gravatar wuestholz2014-09-22
| |
* | fixed various CodeContracts issues.Gravatar qadeer2014-09-18
|/
* mergeGravatar qadeer2014-08-08
|\
* | fixed codexpr bug reported by Michael Emmi; removed special handling of ↵Gravatar qadeer2014-08-08
| | | | | | | | codexpr in InjectPostConditions
| * Bug fix in SIGravatar akashlal2014-08-03
|/
* Some simplificationsGravatar akashlal2014-07-28
|
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
|
* Worked on adding support for "canned errors".Gravatar wuestholz2014-07-07
|
* Added more tests and worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
|
* Worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
|
* Did some refactoring, fixed minor issues, and made it apply the more ↵Gravatar wuestholz2014-07-06
| | | | advanced verification result caching even for implementations with errors.
* Implemented an optimization for assignments to assumption variables that are ↵Gravatar wuestholz2014-07-04
| | | | injected by the verification result caching for calls within loops.
* OnModel now carries the result of the prover callGravatar akashlal2014-06-28
|