Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Did some refactoring. | wuestholz | 2014-09-23 |
| | |||
* | Added key check to uniformity analysis | Ally Donaldson | 2014-05-27 |
| | |||
* | Fixes to predication. Patch by Jeroen Ketema. | Ally Donaldson | 2014-03-18 |
| | |||
* | More exhaustive generation of assertions during predication. Patch by ↵ | Ally Donaldson | 2014-03-14 |
| | | | | Jeroen Ketema | ||
* | Fix to predication | Ally Donaldson | 2014-03-05 |
| | |||
* | (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵ | Rustan Leino | 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. | Ally Donaldson | 2014-01-14 |
| | |||
* | added the QED build configuration | qadeer | 2013-12-02 |
| | |||
* | Fixes to predication. Patch by Jeroen Ketema. | Ally Donaldson | 2013-11-06 |
| | |||
* | Small fix in uniformity analysis | Ally Donaldson | 2013-10-10 |
| | |||
* | Merge | Ally Donaldson | 2013-08-05 |
|\ | |||
* | | Minor changes to uniformity analysis and inter-procedural reachability analysis. | Ally Donaldson | 2013-08-05 |
| | | |||
| * | Fixed several build errors in the 'Checked' configuration. | wuestholz | 2013-08-05 |
|/ | |||
* | ExprSeq: farewell | Ally Donaldson | 2013-07-22 |
| | |||
* | BlockSeq: farewell | Ally Donaldson | 2013-07-22 |
| | |||
* | CmdSeq: farewell | Ally Donaldson | 2013-07-22 |
| | |||
* | Fixes to refactoring | Ally Donaldson | 2013-07-22 |
| | |||
* | Started to remove ...Seq classes | Ally Donaldson | 2013-07-22 |
| | |||
* | More refactoring | Ally Donaldson | 2013-07-22 |
| | |||
* | More refactoring towards replacing PureCollections.Sequence with List | Ally Donaldson | 2013-07-22 |
| | |||
* | merge | Pantazis Deligiannis | 2013-07-22 |
|\ | |||
| * | Requires/EnsuresSeq replaced by List<Requires/Ensures> | Ally Donaldson | 2013-07-22 |
| | | |||
* | | merge | Pantazis Deligiannis | 2013-07-06 |
|\| | |||
| * | Fixed bug with unifomity analysis | allydonaldson | 2013-07-02 |
| | | |||
* | | CVC4 Parser | pantazis | 2013-06-12 |
|/ | |||
* | Staged Houdini | allydonaldson | 2013-04-30 |
| | |||
* | Fixed bug with predication, and fixed small problem with model generation ↵ | allydonaldson | 2013-03-01 |
| | | | | related to casting | ||
* | Support for "do_not_predicate" in predication of requires and ensures | Unknown | 2012-12-20 |
| | |||
* | A simplification to predication of requires and ensures. | Unknown | 2012-11-29 |
| | |||
* | Fixes to uniformity analysis. | Unknown | 2012-11-29 |
| | |||
* | changed the signing to ..\InterimKey.snk | qadeer | 2012-10-03 |
| | |||
* | bunch of refactorings | Unknown | 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 |