summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Collapse)AuthorAge
* Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
| | | | namespaces remain the same.
* Improve support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-09
|
* Add support for weights on soft assumes.Gravatar Valentin Wüstholz2016-03-07
|
* Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
|
* Minor changeGravatar Valentin Wüstholz2015-12-29
|
* Remove workaround for older versions of Z3.Gravatar Valentin Wüstholz2015-12-02
|
* Use the EndCurly token when creating the ReturnCmd for unifiedExitGravatar qunyanm2015-12-02
| | | | | | | | When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block.
* Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
|
* Fix issue with partially-verified assertions.Gravatar Valentin Wüstholz2015-11-19
|
* Add experimental support for optimization (requires Z3 build after changeset ↵Gravatar Valentin Wüstholz2015-11-18
| | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
|
* Add support for annotating implementations with k-ind. depth.Gravatar Valentin Wüstholz2015-10-29
|
* Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-09-30
|
* updateGravatar Shaz Qadeer2015-09-28
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
|\ | | | | | | | | | | | | | | | | | | Conflicts: Source/Core/CommandLineOptions.cs Source/ExecutionEngine/ExecutionEngine.cs Source/ExecutionEngine/VerificationResultCache.cs Source/VCGeneration/VC.cs Test/snapshots/runtest.snapshot Test/snapshots/runtest.snapshot.expect
* | Added /verifySnapshots:3, which prints recycled errors messages with the ↵Gravatar Rustan Leino2015-08-28
| | | | | | | | source locations of the new code.
| * Minor additions to VC genGravatar Akash Lal2015-07-20
| |
| * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | | | | | | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
| * various changes for duality from dead codeplex repoGravatar U-REDMOND\kenmcmil2015-06-09
|/
* Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-05
|
* 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
|
* Make caching of verification results more fine-grained for changes that ↵Gravatar Valentin Wüstholz2015-05-17
| | | | affect preconditions.
* Fix for printFixedPoint when dealing with functionsGravatar Akash Lal2015-05-13
|
* Fix for secureVCGenGravatar Akash Lal2015-05-07
|
* Make it preserve the fact that the value of an assumption variable never ↵Gravatar Valentin Wüstholz2015-05-06
| | | | becomes logically weaker after a havoc.
* 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
|
* Made it produce slightly different passive commands for assignments to ↵Gravatar wuestholz2015-01-30
| | | | assumption variables.
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
|
* Handle timeout in refinement loopGravatar akashlal2015-01-28
|
* Fixed minor issue.Gravatar wuestholz2015-01-26
|
* Minor changeGravatar wuestholz2015-01-26
|
* Worked on the verification result caching (trace output).Gravatar wuestholz2015-01-26
|
* Worked on the verification result caching (use native support for partially ↵Gravatar wuestholz2015-01-16
| | | | verified assertions).
* Fix related to limitations in CVC4 model parsingGravatar Ally Donaldson2015-01-14
|
* Added a test and a todo.Gravatar wuestholz2015-01-02
|
* Worked on more native support for partially-verified assertions.Gravatar wuestholz2014-12-28
|
* Fixed a postcondition.Gravatar wuestholz2014-12-26
|
* Added an annotation, :split_here, for predicate statements.Gravatar Bryan Parno2014-12-16
| | | | | | The annotation allows the programmer to manually indicate where the verification of a procedure implementation should be split into pieces.
* Merge some FixpointVC changes that got left behindGravatar Ken McMillan2014-12-08
|\
* | Optimized the VC generation for assumption variables.Gravatar wuestholz2014-12-07
| |
* | Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-11-10
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-11-05
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-11-03
| |
* | Worked on the verification result caching.Gravatar wuestholz2014-11-03
| |