Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge extra recuresion bound changes for FixedPointVC | 2014-04-21 | |
|\ | |||
* \ | Merge changes for /printFixedPoint option | 2014-04-14 | |
|\ \ | |||
| * | | Added /printFixedPoint option | 2014-04-14 | |
| | | | |||
* | | | resolved expressions created during generation of procedures for mover checks | 2014-04-14 | |
| | | | |||
* | | | Fixed abstract interpretation for reals | 2014-04-13 | |
|/ / | |||
* | | Fixed bug in abstract interpretation over reals | 2014-04-08 | |
| | | |||
* | | Added option to avoid unrolling irreducible loops | 2014-04-06 | |
| | | |||
* | | Fixed class cast issue with type synonyms | 2014-04-01 | |
| | | |||
* | | Fixes to predication. Patch by Jeroen Ketema. | 2014-03-18 | |
| | | |||
| * | Added extra recursion bound and preconditions to FixedpointVC. | 2014-03-17 | |
| | | |||
* | | Change class 'LambdaVisitor' to attach checksum to expanded lambda functions. | 2014-03-17 | |
| | | |||
* | | More exhaustive generation of assertions during predication. Patch by ↵ | 2014-03-14 | |
| | | | | | | | | Jeroen Ketema | ||
* | | Fix duplicator so that BVConcatExpr and BVExtractExpr are handled. Patch by ↵ | 2014-03-12 | |
| | | | | | | | | Daniel Liew. | ||
* | | Fix to predication | 2014-03-05 | |
| | | |||
* | | Merge | 2014-02-28 | |
|\ \ | |||
* | | | Changed all lambda-expression rewriting to be done as a pre-processing step ↵ | 2014-02-28 | |
| | | | | | | | | | | | | | | | | | | before real verification. Fixed treatment of lambda-expression attributes. | ||
| * | | Added a fix to inlining so that it becomes cognizant of procedures that the ↵ | 2014-02-28 | |
| | | | | | | | | | | | | user wants to check | ||
| * | | Added /trustNonInterference option | 2014-02-28 | |
| | | | |||
* | | | Changed return type of VisitLambdaExpr to just Expr | 2014-02-27 | |
| | | | |||
| * | | added /doNotUseParallelism option | 2014-02-27 | |
| | | | |||
| * | | added some missing attributes to desugared assertions | 2014-02-27 | |
|/ / | |||
* | | added tokens to calls and requires/ensures | 2014-02-26 | |
| | | |||
* | | Merge | 2014-02-25 | |
|\ \ | |||
* | | | fixed couple of bugs reported by Serdar | 2014-02-25 | |
| | | | |||
| * | | Fixed tokens to improve error message produce for type errors in non-inlined ↵ | 2014-02-25 | |
|/ / | | | | | | | function bodies | ||
* | | (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. | ||
* | | added ReadOnlyStandardVisitor | 2014-02-24 | |
| | | | | | | | | made the default phase of assertions be 0 | ||
* | | Added /trustPhasesDownto option | 2014-02-24 | |
| | | |||
* | | Added /trustPhasesUpto option | 2014-02-23 | |
| | | |||
* | | Added /trustAtomicityTypes option | 2014-02-22 | |
|/ | |||
* | Merge ModelParser fix | 2014-02-21 | |
|\ | |||
| * | Fixed crash in ModelParser when Z3 returns an operator that is a list. | 2014-02-21 | |
| | | |||
* | | fixed a bug in desugaring of linear variables | 2014-02-20 | |
|/ | |||
* | Merge fixedpoint VC fix | 2014-02-19 | |
|\ | |||
| * | Fixedpoint VC fix. | 2014-02-19 | |
| | | |||
* | | fixed a bug in the automaton construction labeling | 2014-02-18 | |
| | | |||
* | | fixed code contracts violations | 2014-02-11 | |
| | | |||
* | | Fixed bug in printing real literals | 2014-02-10 | |
| | | |||
* | | Fixed errors in the use of Code Contracts | 2014-02-10 | |
| | | |||
* | | Merge | 2014-02-10 | |
|\ \ | |||
* | | | Fixed bug in handling of break statements | 2014-02-10 | |
| | | | |||
| * | | fixed a problem with the nonblocking check | 2014-02-10 | |
| | | | |||
| * | | added nonblocking checker for left movers | 2014-02-07 | |
| | | | |||
| * | | added another example and fixed a bug regarding initialization of pc/ok | 2014-02-07 | |
| | | | | | | | | | | | | snapshots per loop header | ||
| * | | new design for linear types + VCgen | 2014-02-07 | |
|/ / | | | | | | | | | ported all the examples added the QED examples to runtest.bat | ||
* | | bug fix in error trace printing | 2014-02-05 | |
| | | | | | | | | added a class for Token elimination (not done yet) | ||
* | | Option for reversing Houdini worklist (for top-down analysis) | 2014-01-28 | |
| | | |||
* | | some small optimizations to mover checking | 2014-01-22 | |
| | | | | | | | | added LookUp to multiset.bpl | ||
* | | various bug fixes | 2014-01-21 | |
| | | | | | | | | added "cnst" feature | ||
* | | bug fix: if an absy is not reachable, make the set of available vars empty at it | 2014-01-21 | |
| | |