summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* Work stealing queue (PLDI '12 Vechev et al.)Gravatar Unknown2015-01-28
|
* Handle timeout in refinement loopGravatar akashlal2015-01-28
|
* MergeGravatar qadeer2015-01-27
|\
* | removed unused functions and axioms to make the verification fasterGravatar qadeer2015-01-27
| |
| * Fixed minor issue.Gravatar wuestholz2015-01-26
| |
| * Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26
| |
| * Minor changeGravatar wuestholz2015-01-26
| |
| * Minor changeGravatar wuestholz2015-01-26
| |
| * Worked on the verification result caching (trace output).Gravatar wuestholz2015-01-26
| |
| * Change the return type of StandardVisitor.VisitLiteralExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | LiteralExpr to Expr. Enforcing the return type be LiteralExpr is too restrictive. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitExistsExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | ExistsExpr to Expr. Enforcing the return type be ExistsExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitForAllExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | ForAllExpr to Expr. Enforcing the return type be ForAllExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitBvExtractExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitBvConcatExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type.
| * Worked on the verification result caching (use weights for extracted functions).Gravatar wuestholz2015-01-24
| |
| * Worked on the verification result caching (use native support for partially ↵Gravatar wuestholz2015-01-16
| | | | | | | | verified assertions).
| * Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-23
| |
| * MergeGravatar Ally Donaldson2015-01-22
| |\ | |/ |/|
| * Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-22
| |
* | MergeGravatar qadeer2015-01-16
|\|
* | removed "layer" attribute from the desugared programGravatar qadeer2015-01-16
| |
| * Worked on StagedHoudiniGravatar Ally Donaldson2015-01-16
| |
| * Fix related to limitations in CVC4 model parsingGravatar Ally Donaldson2015-01-14
| |
| * MergeGravatar Ally Donaldson2015-01-13
| |\
| | * Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
| | |\
| | * | Merging changes from 0biha/BoogieInvariantFixesIIIaGravatar wuestholz2015-01-13
| |/| | |/| | |
| * | | Removed unnecessary stage-related attributes from candidate annotations.Gravatar Ally Donaldson2015-01-10
| | | |
| | | * Made 2 invariants of class 'VariableCollector' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field protected - exposing IEnumerables (with help from David Rohr)
| | | * Made invariant of class 'Trigger' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - adding getter/setter - copying incoming list - exposing read-only list (with help from David Rohr)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private and readonly - exposing IEnumerable - adding 'AddLabel' method (with help from David Rohr)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - adding private field - exposing read-only list - copying incoming list (with help from David Rohr)
| | | * Made invariant of class 'QKeyValue' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing read-only list - copying incoming list - adding methods 'AddParam', 'AddParams', and 'ClearParams' (with help from David Rohr)
| | | * Made invariant of class 'EEDTemplate' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable - copying incoming list (with help from David Rohr)
| | | * Made invariant of class 'Block' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr)
| | | * Made invariant of class CommandLineOptions robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr)
| | | * 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)
* | | Minor changes to the "Checked" build configurationGravatar wuestholz2015-01-09
|/ /
| * Tiny change ('Trigger' class)Gravatar 0biha2015-01-08
| |
* | Updated to Staged HoudiniGravatar Ally Donaldson2015-01-08
| |
| * Fixed a null reference problem in class 'Constant'.Gravatar 0biha2015-01-08
| |
| * Tiny fix (made field 'tr' of class 'Trigger' private)Gravatar 0biha2015-01-08
| |
| * Made 2 invariants of class 'DeclWithFormals' robust by changing the designGravatar 0biha2015-01-07
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Rewrote 'globalVariablesCache' invariant fix of class 'Program'Gravatar 0biha2015-01-08
| |
| * Made invariant of class 'Constant' robust by making list 'Parents' read-onlyGravatar 0biha2015-01-05
| |
| * Made invariant of class 'AtomicRE' robust by changing the designGravatar 0biha2015-01-05
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made invariant of class 'Trigger' robust byGravatar 0biha2015-01-01
| | | | | | | | | | | | -replacing public field by private field + getter -using read-only wrappers (to avoid leaking) -cloning the tr list in the setter and constructor (to avoid capturing)
| * Made invariant of class 'ListOfMiningStrategies' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made invariant of class 'IfThenElse' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made 2 invariants of class 'IfCmd' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Made invariant of class 'EEDTemplate' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-03 14:55:35 +0000