summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* second checkpointGravatar qadeer2014-05-04
|
* checkpointGravatar qadeer2014-05-03
|
* bug fix in the last updateGravatar qadeer2014-04-25
|
* updated the mover checksGravatar qadeer2014-04-25
|
* Add support for assumption variables.Gravatar wuestholz2014-04-21
|
* added another sampleGravatar qadeer2014-04-20
|
* added simulation relation computation to yield type checkingGravatar qadeer2014-04-20
| | | | updated the type check to incorporate {:terminates} annotation
* fixed some bugs in the previous check insGravatar qadeer2014-04-16
|
* added the framing for the refinement checkGravatar qadeer2014-04-16
|
* MergeGravatar qadeer2014-04-16
|\
* | added variable hidingGravatar qadeer2014-04-16
| | | | | | | | added annotation on an atomic action about the phases in which it exists
| * Minor fix to abshoudiniGravatar akashlal2014-04-16
| |
| * Fixed malformed Contracts sectionGravatar Rustan Leino2014-04-15
| |
| * disabled quantifier merging, except when no triggers are provided (as ↵Gravatar Unknown2014-03-03
|/ | | | discussed with Rustan)
* MergeGravatar qadeer2014-04-15
|\
* | added more types to constructed expressionsGravatar qadeer2014-04-15
| |
| * Merge changes for /printFixedPoint optionGravatar Ken McMillan2014-04-14
|/|
| * Added /printFixedPoint optionGravatar Ken McMillan2014-04-14
| |
* | resolved expressions created during generation of procedures for mover checksGravatar qadeer2014-04-14
| |
* | Fixed abstract interpretation for realsGravatar Rustan Leino2014-04-13
|/
* Fixed bug in abstract interpretation over realsGravatar Rustan Leino2014-04-08
|
* Added option to avoid unrolling irreducible loopsGravatar akashlal2014-04-06
|
* Fixed class cast issue with type synonymsGravatar Ally Donaldson2014-04-01
|
* Fixes to predication. Patch by Jeroen Ketema.Gravatar Ally Donaldson2014-03-18
|
* Change class 'LambdaVisitor' to attach checksum to expanded lambda functions.Gravatar wuestholz2014-03-17
|
* More exhaustive generation of assertions during predication. Patch by ↵Gravatar Ally Donaldson2014-03-14
| | | | Jeroen Ketema
* Fix duplicator so that BVConcatExpr and BVExtractExpr are handled. Patch by ↵Gravatar Ally Donaldson2014-03-12
| | | | Daniel Liew.
* Fix to predicationGravatar Ally Donaldson2014-03-05
|
* MergeGravatar Rustan Leino2014-02-28
|\
* | Changed all lambda-expression rewriting to be done as a pre-processing step ↵Gravatar Rustan Leino2014-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 ↵Gravatar qadeer2014-02-28
| | | | | | | | user wants to check
| * Added /trustNonInterference optionGravatar qadeer2014-02-28
| |
* | Changed return type of VisitLambdaExpr to just ExprGravatar Rustan Leino2014-02-27
| |
| * added /doNotUseParallelism optionGravatar qadeer2014-02-27
| |
| * added some missing attributes to desugared assertionsGravatar qadeer2014-02-27
|/
* added tokens to calls and requires/ensuresGravatar qadeer2014-02-26
|
* MergeGravatar qadeer2014-02-25
|\
* | fixed couple of bugs reported by SerdarGravatar qadeer2014-02-25
| |
| * Fixed tokens to improve error message produce for type errors in non-inlined ↵Gravatar Rustan Leino2014-02-25
|/ | | | function bodies
* (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.
* added ReadOnlyStandardVisitorGravatar qadeer2014-02-24
| | | | made the default phase of assertions be 0
* Added /trustPhasesDownto optionGravatar qadeer2014-02-24
|
* Added /trustPhasesUpto optionGravatar qadeer2014-02-23
|
* Added /trustAtomicityTypes optionGravatar qadeer2014-02-22
|
* Merge ModelParser fixGravatar Ken McMillan2014-02-21
|\
| * Fixed crash in ModelParser when Z3 returns an operator that is a list.Gravatar Ken McMillan2014-02-21
| |
* | fixed a bug in desugaring of linear variablesGravatar qadeer2014-02-20
|/
* Merge fixedpoint VC fixGravatar Ken McMillan2014-02-19
|\
| * Fixedpoint VC fix.Gravatar Ken McMillan2014-02-19
| |
* | fixed a bug in the automaton construction labelingGravatar qadeer2014-02-18
| |