Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Rename DLLs to non-generic names by prefixing "Boogie". Project names and | akashlal | 2016-04-15 |
| | | | | namespaces remain the same. | ||
* | Improve support for identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-09 |
| | |||
* | Add support for weights on soft assumes. | Valentin Wüstholz | 2016-03-07 |
| | |||
* | Improve support for optimization and identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-03 |
| | |||
* | Minor change | Valentin Wüstholz | 2015-12-29 |
| | |||
* | Remove workaround for older versions of Z3. | Valentin Wüstholz | 2015-12-02 |
| | |||
* | Use the EndCurly token when creating the ReturnCmd for unifiedExit | qunyanm | 2015-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. | Valentin Wüstholz | 2015-11-20 |
| | |||
* | Fix issue with partially-verified assertions. | Valentin Wüstholz | 2015-11-19 |
| | |||
* | Add experimental support for optimization (requires Z3 build after changeset ↵ | Valentin Wüstholz | 2015-11-18 |
| | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
* | Add support for identifying unnecessary assumes. | Valentin Wüstholz | 2015-11-16 |
| | |||
* | Add support for annotating implementations with k-ind. depth. | Valentin Wüstholz | 2015-10-29 |
| | |||
* | Improve output for diagnosing timeouts. | Valentin Wüstholz | 2015-09-30 |
| | |||
* | update | Shaz Qadeer | 2015-09-28 |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | Rustan Leino | 2015-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 ↵ | Rustan Leino | 2015-08-28 |
| | | | | | | | | source locations of the new code. | ||
| * | Minor additions to VC gen | Akash Lal | 2015-07-20 |
| | | |||
| * | Normalise line endings using a .gitattributes file. Unfortunately | Dan Liew | 2015-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 repo | U-REDMOND\kenmcmil | 2015-06-09 |
|/ | |||
* | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-06-05 |
| | |||
* | Fix for SI: initialize extraRecBound | Akash Lal | 2015-06-05 |
| | |||
* | Simplified StratifiedVC interface | akashlal | 2015-06-01 |
| | |||
* | Allow for extra instrumentation on program before vc gen | Akash Lal | 2015-05-25 |
| | |||
* | Add some experimental support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-18 |
| | |||
* | Make caching of verification results more fine-grained for changes that ↵ | Valentin Wüstholz | 2015-05-17 |
| | | | | affect preconditions. | ||
* | Fix for printFixedPoint when dealing with functions | Akash Lal | 2015-05-13 |
| | |||
* | Fix for secureVCGen | Akash Lal | 2015-05-07 |
| | |||
* | Make it preserve the fact that the value of an assumption variable never ↵ | Valentin Wüstholz | 2015-05-06 |
| | | | | becomes logically weaker after a havoc. | ||
* | VC gen for security properties | akashlal | 2015-04-05 |
| | |||
* | Compute MustReach information lazily, on-demand | akashlal | 2015-03-16 |
| | |||
* | Added MustReach information to VC gen | akashlal | 2015-03-11 |
| | |||
* | Made it produce slightly different passive commands for assignments to ↵ | wuestholz | 2015-01-30 |
| | | | | assumption variables. | ||
* | Minor change to the encoding of partially verified assertions as VC | wuestholz | 2015-01-30 |
| | |||
* | Handle timeout in refinement loop | akashlal | 2015-01-28 |
| | |||
* | Fixed minor issue. | wuestholz | 2015-01-26 |
| | |||
* | Minor change | wuestholz | 2015-01-26 |
| | |||
* | Worked on the verification result caching (trace output). | wuestholz | 2015-01-26 |
| | |||
* | Worked on the verification result caching (use native support for partially ↵ | wuestholz | 2015-01-16 |
| | | | | verified assertions). | ||
* | Fix related to limitations in CVC4 model parsing | Ally Donaldson | 2015-01-14 |
| | |||
* | Added a test and a todo. | wuestholz | 2015-01-02 |
| | |||
* | Worked on more native support for partially-verified assertions. | wuestholz | 2014-12-28 |
| | |||
* | Fixed a postcondition. | wuestholz | 2014-12-26 |
| | |||
* | Added an annotation, :split_here, for predicate statements. | Bryan Parno | 2014-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 behind | Ken McMillan | 2014-12-08 |
|\ | |||
* | | Optimized the VC generation for assumption variables. | wuestholz | 2014-12-07 |
| | | |||
* | | Fixed issue in the verification result caching. | wuestholz | 2014-11-10 |
| | | |||
* | | Worked on the verification result caching. | wuestholz | 2014-11-10 |
| | | |||
* | | Worked on the verification result caching. | wuestholz | 2014-11-05 |
| | | |||
* | | Worked on the verification result caching. | wuestholz | 2014-11-03 |
| | | |||
* | | Worked on the verification result caching. | wuestholz | 2014-11-03 |
| | |