Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | factored the concurrency checking code into a separate project | 2013-11-22 | |
| | |||
* | code cleanup | 2013-11-02 | |
| | |||
* | Merge | 2013-10-25 | |
|\ | |||
* | | minor refactoring | 2013-10-25 | |
| | | | | | | | | moved the call to EliminateDeadVariablesAndInline to after the OG sequentialization | ||
* | | a minor refactoring + implemented mover checking | 2013-10-25 | |
| | | |||
| * | Stratified inlining: inject free requires as assumes at call site | 2013-10-25 | |
| | | |||
| * | change of identifier names in OG | 2013-10-25 | |
|/ | |||
* | 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-09 | |
| |\ | |/ |/| | |||
| * | small refactoring | 2013-10-02 | |
| | | |||
| * | support for disabling loop entry invariant assertion checking | 2013-10-01 | |
| | | |||
| * | changes to support a configured errorLimit | 2013-09-30 | |
| | | |||
| * | more changes towards parallelisation of Houdini | 2013-09-29 | |
| | | |||
| * | 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 | |
| | | |||
* | | 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 | |
| |\ | |/ |/| | |||
| * | 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 | |
| | | |||
* | | 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 | ||
* | | 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 | |
|/ / | |||
* | | added proper resolution and typechecking for all generated expressions | 2013-07-29 | |
| | | |||
* | | added types for all the expressions being added to calls | 2013-07-29 | |
| | | |||
| * | parallel houdini prototype working | 2013-07-26 | |
|/ | |||
* | Removed the remaining pure collections. | 2013-07-23 | |
| | |||
* | Resolved some issues with data races. | 2013-07-23 | |
| | |||
* | Did some refactoring. | 2013-07-23 | |
| | |||
* | Did some refactoring. | 2013-07-23 | |
| | |||
* | Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵ | 2013-07-22 | |
| | | | | code (as opposed to contracts). | ||
* | Fixed the Coco/R grammar and regenerated the parser. | 2013-07-22 | |
| | |||
* | All ...Seq classes now gone | 2013-07-22 | |
| | |||
* | ExprSeq: farewell | 2013-07-22 | |
| | |||
* | RESeq: farewell | 2013-07-22 | |
| | |||
* | BlockSeq: farewell | 2013-07-22 | |
| | |||
* | StringSeq: 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 | 2013-07-22 | |
| |