summaryrefslogtreecommitdiff
path: root/Source/Houdini
Commit message (Collapse)AuthorAge
* MergeGravatar Ally Donaldson2015-01-13
|\
* | Removed unnecessary stage-related attributes from candidate annotations.Gravatar Ally Donaldson2015-01-10
| |
| * Made 2 invariants of class 'CommandLineOptions' robust by:Gravatar wuestholz2015-01-09
|/ | | | | | | - making fields private - exposing IEnumerables - adding methods 'AddProverOption', 'RemoveAllProverOptions', and 'AddZ3Option' (with help from David Rohr)
* Updated to Staged HoudiniGravatar Ally Donaldson2015-01-08
|
* changed the suffix of the trace file from .bpl to .txt to avoid confusing ↵Gravatar qadeer2014-11-08
| | | | the lit tool
* Lets have a setter for TopLevelDeclarations as wellGravatar akashlal2014-09-25
|
* Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
|
* Did more refactoring.Gravatar wuestholz2014-09-23
|
* Did some refactoring.Gravatar wuestholz2014-09-23
|
* minor fix to abshoudini's handling of quantifiersGravatar akashlal2014-09-20
|
* a bug fix in Houdini (also AbsHoudini)Gravatar qadeer2014-09-19
|
* InlineAssume attribute for ensures clauses; if present, the ensures ↵Gravatar qadeer2014-09-18
| | | | condition is assumed while inlining.
* fixed a bug in inliningGravatar qadeer2014-09-17
| | | | changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"
* fixed a crashGravatar qadeer2014-09-16
|
* ExplainHoudini change to add reasons for inconsistency as well.Gravatar shuvendu2014-07-27
|
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-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 callGravatar akashlal2014-06-28
|
* Refactored ConcurrentHoudini and Houdini to (significantly) reduce ↵Gravatar Ally Donaldson2014-05-28
| | | | duplication of code
* Removed printing code from candidate dependence analyserGravatar Ally Donadlson2014-05-28
|
* Small cleanup in Staged HoudiniGravatar Ally Donaldson2014-05-28
|
* Fixed state capture concurrency bug with Staged HoudiniGravatar Ally Donaldson2014-05-27
|
* Minor fix to abshoudiniGravatar akashlal2014-04-16
|
* (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵Gravatar Rustan Leino2014-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 ContractsGravatar Rustan Leino2014-02-10
|
* Option for reversing Houdini worklist (for top-down analysis)Gravatar akashlal2014-01-28
|
* Recursive walking of Exprs doesn't play nice when the depth of the AST is high.Gravatar akashlal2014-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 configurationGravatar qadeer2013-12-02
|
* binary tree of ANDs saves stack spaceGravatar akashlal2013-11-29
|
* MergeGravatar Pantazis Deligiannis2013-11-07
|\
| * AbsHoudini: Support timeout, MakeTop, InlineFunctionsGravatar akashlal2013-11-02
| |
* | small fix in the parallel refutation sharingGravatar Pantazis Deligiannis2013-10-16
|/
* small cleanupGravatar Pantazis Deligiannis2013-10-10
|
* fixed bug with the exchange refuted invariants processGravatar Pantazis Deligiannis2013-10-06
|
* small refactoringGravatar Pantazis Deligiannis2013-10-02
|
* removal of commentGravatar Pantazis Deligiannis2013-10-02
|
* fixed bugGravatar Pantazis Deligiannis2013-10-01
|
* changes to support a configured errorLimitGravatar Pantazis Deligiannis2013-09-30
|
* more changes towards parallelisation of HoudiniGravatar Pantazis Deligiannis2013-09-29
|
* refactoring + new class ConcurrentHoudiniGravatar Pantazis Deligiannis2013-09-27
|
* refuted candidates are exchanged in memory using a concurrent dictionary ↵Gravatar Pantazis Deligiannis2013-09-26
| | | | instead of using an IO csv file as before
* improvements to the refuted annotations exchange processGravatar Pantazis Deligiannis2013-08-20
|
* new option for reversing the topological order - this could potentially help ↵Gravatar Pantazis Deligiannis2013-08-19
| | | | to speedup houdini refutation of candidates
* changes in the parallel houdini scriptGravatar Pantazis Deligiannis2013-07-30
|
* added script for running the portfolio solver (parallel houdini)Gravatar Pantazis Deligiannis2013-07-30
|
* parallel houdini prototype workingGravatar Pantazis Deligiannis2013-07-26
|
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
|
* CmdSeq: farewellGravatar Ally Donaldson2013-07-22
|
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
|
* More refactoringGravatar Ally Donaldson2013-07-22
|
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-29 00:26:56 +0000