Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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. | ||
* | Missing braces | 2015-06-20 | |
| | |||
* | Minor changes | 2015-05-20 | |
| | |||
* | Fix for AbsHoudini | 2015-05-01 | |
| | |||
* | AbsHoudini: made disjunct bound a parameter | 2015-05-01 | |
| | |||
* | Minor fixes for AbsHoudini | 2015-04-23 | |
| | |||
* | Better error message | 2015-04-21 | |
| | |||
* | Eliminated calls to deprecated method. | 2015-02-18 | |
| | |||
* | Fixes to StagedHoudini | 2015-01-23 | |
| | |||
* | Fixes to StagedHoudini | 2015-01-22 | |
| | |||
* | Worked on StagedHoudini | 2015-01-16 | |
| | |||
* | Merge | 2015-01-13 | |
|\ | |||
* | | Removed unnecessary stage-related attributes from candidate annotations. | 2015-01-10 | |
| | | |||
| * | Made 2 invariants of class 'CommandLineOptions' robust by: | 2015-01-09 | |
|/ | | | | | | | - making fields private - exposing IEnumerables - adding methods 'AddProverOption', 'RemoveAllProverOptions', and 'AddZ3Option' (with help from David Rohr) | ||
* | Updated to Staged Houdini | 2015-01-08 | |
| | |||
* | changed the suffix of the trace file from .bpl to .txt to avoid confusing ↵ | 2014-11-08 | |
| | | | | the lit tool | ||
* | Lets have a setter for TopLevelDeclarations as well | 2014-09-25 | |
| | |||
* | Did more refactoring and addressed several todos. | 2014-09-23 | |
| | |||
* | Did more refactoring. | 2014-09-23 | |
| | |||
* | Did some refactoring. | 2014-09-23 | |
| | |||
* | minor fix to abshoudini's handling of quantifiers | 2014-09-20 | |
| | |||
* | a bug fix in Houdini (also AbsHoudini) | 2014-09-19 | |
| | |||
* | InlineAssume attribute for ensures clauses; if present, the ensures ↵ | 2014-09-18 | |
| | | | | condition is assumed while inlining. | ||
* | fixed a bug in inlining | 2014-09-17 | |
| | | | | changed the attribute on callee ensures to "HoudiniAssume" rather than "assume" | ||
* | fixed a crash | 2014-09-16 | |
| | |||
* | ExplainHoudini change to add reasons for inconsistency as well. | 2014-07-27 | |
| | |||
* | Fix nasty bug introduced by commit 61a94f409975. | 2014-07-15 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs. | ||
* | OnModel now carries the result of the prover call | 2014-06-28 | |
| | |||
* | Refactored ConcurrentHoudini and Houdini to (significantly) reduce ↵ | 2014-05-28 | |
| | | | | duplication of code | ||
* | Removed printing code from candidate dependence analyser | 2014-05-28 | |
| | |||
* | Small cleanup in Staged Houdini | 2014-05-28 | |
| | |||
* | Fixed state capture concurrency bug with Staged Houdini | 2014-05-27 | |
| | |||
* | Minor fix to abshoudini | 2014-04-16 | |
| | |||
* | (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. | ||
* | Fixed errors in the use of Code Contracts | 2014-02-10 | |
| | |||
* | Option for reversing Houdini worklist (for top-down analysis) | 2014-01-28 | |
| | |||
* | Recursive walking of Exprs doesn't play nice when the depth of the AST is high. | 2014-01-07 | |
| | | | | | Reduce depth of AST whenever possible (e.g., use a binary tree instead of a linear list of terms) | ||
* | added the QED build configuration | 2013-12-02 | |
| | |||
* | binary tree of ANDs saves stack space | 2013-11-29 | |
| | |||
* | Merge | 2013-11-07 | |
|\ | |||
| * | AbsHoudini: Support timeout, MakeTop, InlineFunctions | 2013-11-02 | |
| | | |||
* | | small fix in the parallel refutation sharing | 2013-10-16 | |
|/ | |||
* | small cleanup | 2013-10-10 | |
| | |||
* | fixed bug with the exchange refuted invariants process | 2013-10-06 | |
| | |||
* | small refactoring | 2013-10-02 | |
| | |||
* | removal of comment | 2013-10-02 | |
| | |||
* | 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 | |
| |