Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | 2013-10-15 | |
|\ | |||
* | | bug fix in yield inference in modset analysis | 2013-10-15 | |
| | | |||
| * | Fix for the Duplicator. | 2013-10-15 | |
| | | |||
| * | Merge | 2013-10-11 | |
| |\ | |||
| * | | Small fix in uniformity analysis | 2013-10-10 | |
| | | | |||
| | * | Merge | 2013-10-10 | |
| | |\ | | |/ | |/| | |||
| | * | small cleanup | 2013-10-10 | |
| | | | |||
| * | | Merge | 2013-10-09 | |
| |\ \ | |/ / |/| / | |/ | |||
| * | fixed bug with the exchange refuted invariants process | 2013-10-06 | |
| | | |||
| * | small refactoring | 2013-10-02 | |
| | | |||
| * | removal of comment | 2013-10-02 | |
| | | |||
| * | support for disabling loop entry invariant assertion checking | 2013-10-01 | |
| | | |||
| * | fixed bug | 2013-10-01 | |
| | | |||
| * | changes to support a configured errorLimit | 2013-09-30 | |
| | | |||
| * | more changes towards parallelisation of Houdini | 2013-09-29 | |
| | | |||
| * | refactoring + new class ConcurrentHoudini | 2013-09-27 | |
| | | |||
| * | refuted candidates are exchanged in memory using a concurrent dictionary ↵ | 2013-09-26 | |
| | | | | | | | | instead of using an IO csv file as before | ||
* | | minor fix so that variable copies in procedures and codeexprs are different. | 2013-09-10 | |
| | | |||
* | | refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of ↵ | 2013-09-09 | |
| | | | | | | | | GenerateVC | ||
* | | fixed bug | 2013-09-09 | |
| | | |||
* | | No need for OG with Stratified Inlining. | 2013-09-08 | |
| | | |||
* | | fixed bug introduced by the last checkin in letvciterative | 2013-09-08 | |
| | | | | | | | | added /vc:i to all tests in stratifiedinline | ||
* | | fixed the problem with codexprs | 2013-09-07 | |
| | | | | | | | | now positive/negative context is detected and appropriate translation is done | ||
* | | When a codeexpr is used at the top-level in an assume statement, we use the ↵ | 2013-09-04 | |
| | | | | | | | | alternative existential semantics. | ||
* | | Factored out the closure for codeexpr conversion so that it can be reused. | 2013-09-04 | |
| | | | | | | | | Enabled it in stratified inlining. | ||
* | | fixed the linear type checking related to globals | 2013-09-04 | |
| | | | | | | | | | | fixed the modset analysis so that it infers the stable predicate also added more information to type error messages | ||
* | | Applied Chris Hawblitzel's changes to deal with {:expand} | 2013-08-23 | |
| | | | | | | | | Erased {:yields} in the resulting sequential program in OwickiGriesTransform | ||
* | | some minor fixes | 2013-08-21 | |
| | | |||
| * | Merge | 2013-08-20 | |
| |\ | |/ |/| | |||
| * | improvements to the refuted annotations exchange process | 2013-08-20 | |
| | | |||
| * | new option for reversing the topological order - this could potentially help ↵ | 2013-08-19 | |
| | | | | | | | | to speedup houdini refutation of candidates | ||
* | | inlining is now done in rhs of assignments for codeexprs | 2013-08-15 | |
| | | | | | | | | added more regressions | ||
* | | Extended codeexpr inlining to deal with nested codeexpr | 2013-08-15 | |
| | | | | | | | | Added a regression | ||
| * | new option to disable checking for loop maintained invariants - this leads ↵ | 2013-08-15 | |
| | | | | | | | | to an underapproximation that helps to speedup houdini refutation of candidates | ||
* | | extended inlining to deal with codeexprs | 2013-08-14 | |
| | | |||
* | | Fixed a contract. | 2013-08-09 | |
| | | |||
* | | process procedure only if an implementation is present. | 2013-08-07 | |
| | | |||
* | | cleaned up the OG code | 2013-08-07 | |
| | | | | | | | | enabled it to be always on | ||
* | | Changed BVD to display shortened names if they are unique. | 2013-08-05 | |
| | | |||
* | | 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 | |
| | | | |||
| * | | Reverted change to use MODEL_ON_FINAL_CHECK, which seems to cause Z3 ↵ | 2013-08-02 | |
| | | | | | | | | | | | | unexpectedly to output model information | ||
| * | | Turned on options in Z3 to try producing models for timeouts. | 2013-08-02 | |
| | | | |||
| * | | Make it possible to set the font in BVD externally. | 2013-07-31 | |
|/ / | |||
* | | Make it possible to look up variables in the Dafny error models. | 2013-07-30 | |
| | | |||
* | | Added test cases for symdiff (z3multipleErrors flag) | 2013-07-30 | |
| | | |||
| * | changes in the parallel houdini script | 2013-07-30 | |
| | | |||
* | | Make the dependency analysis for snapshot verification take 'where' clauses ↵ | 2013-07-30 | |
| | | | | | | | | into account. | ||
| * | added script for running the portfolio solver (parallel houdini) | 2013-07-30 | |
| | |