summaryrefslogtreecommitdiff
path: root/Source/Houdini
Commit message (Collapse)AuthorAge
* Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
| | | | namespaces remain the same.
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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 bracesGravatar akashlal2015-06-20
|
* Minor changesGravatar Valentin Wüstholz2015-05-20
|
* Fix for AbsHoudiniGravatar akashlal2015-05-01
|
* AbsHoudini: made disjunct bound a parameterGravatar akashlal2015-05-01
|
* Minor fixes for AbsHoudiniGravatar Akash Lal2015-04-23
|
* Better error messageGravatar akashlal2015-04-21
|
* Eliminated calls to deprecated method.Gravatar wuestholz2015-02-18
|
* Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-23
|
* Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-22
|
* Worked on StagedHoudiniGravatar Ally Donaldson2015-01-16
|
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-25 23:32:20 +0000