Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Rename DLLs to non-generic names by prefixing "Boogie". Project names and | 2016-04-15 | |
| | | | | namespaces remain the same. | ||
* | Normalise line endings using a .gitattributes file. Unfortunately | 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. | ||
* | Patch by Jeroen Ketema. | 2015-04-05 | |
| | | | | | | Drop the “basic” block predication algorithm. Block predication is only used by GPUVerify, and then only in the “smart” version as the basic algorithm does not perform very well. As a consequence this code is essentially dead. | ||
* | Patch by Jeroen Ketema | 2015-03-27 | |
| | | | | Expose information about the predicate assigned to the immediate dominator of a CFG node. | ||
* | Minor changes to the "Checked" build configuration | 2015-01-09 | |
| | |||
* | Did some refactoring. | 2014-09-23 | |
| | |||
* | Added key check to uniformity analysis | 2014-05-27 | |
| | |||
* | Fixes to predication. Patch by Jeroen Ketema. | 2014-03-18 | |
| | |||
* | More exhaustive generation of assertions during predication. Patch by ↵ | 2014-03-14 | |
| | | | | Jeroen Ketema | ||
* | Fix to predication | 2014-03-05 | |
| | |||
* | (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵ | 2014-02-24 | |
| | | | | | | of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor. | ||
* | Fix Boogie so it compiled with mono. Patch by Dan Liew. | 2014-01-14 | |
| | |||
* | added the QED build configuration | 2013-12-02 | |
| | |||
* | Fixes to predication. Patch by Jeroen Ketema. | 2013-11-06 | |
| | |||
* | Small fix in uniformity analysis | 2013-10-10 | |
| | |||
* | Merge | 2013-08-05 | |
|\ | |||
* | | Minor changes to uniformity analysis and inter-procedural reachability analysis. | 2013-08-05 | |
| | | |||
| * | Fixed several build errors in the 'Checked' configuration. | 2013-08-05 | |
|/ | |||
* | ExprSeq: farewell | 2013-07-22 | |
| | |||
* | BlockSeq: farewell | 2013-07-22 | |
| | |||
* | CmdSeq: farewell | 2013-07-22 | |
| | |||
* | Fixes to refactoring | 2013-07-22 | |
| | |||
* | Started to remove ...Seq classes | 2013-07-22 | |
| | |||
* | More refactoring | 2013-07-22 | |
| | |||
* | More refactoring towards replacing PureCollections.Sequence with List | 2013-07-22 | |
| | |||
* | merge | 2013-07-22 | |
|\ | |||
| * | Requires/EnsuresSeq replaced by List<Requires/Ensures> | 2013-07-22 | |
| | | |||
* | | merge | 2013-07-06 | |
|\| | |||
| * | Fixed bug with unifomity analysis | 2013-07-02 | |
| | | |||
* | | CVC4 Parser | 2013-06-12 | |
|/ | |||
* | Staged Houdini | 2013-04-30 | |
| | |||
* | Fixed bug with predication, and fixed small problem with model generation ↵ | 2013-03-01 | |
| | | | | related to casting | ||
* | Support for "do_not_predicate" in predication of requires and ensures | 2012-12-20 | |
| | |||
* | A simplification to predication of requires and ensures. | 2012-11-29 | |
| | |||
* | Fixes to uniformity analysis. | 2012-11-29 | |
| | |||
* | changed the signing to ..\InterimKey.snk | 2012-10-03 | |
| | |||
* | bunch of refactorings | 2012-10-03 | |
- moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs |