summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
...
* | Core: attach :partition to assumes generated from structured ifs and whilesGravatar Peter Collingbourne2012-08-03
|/
* Dafny: fixed bug in reverifying allowing old locals to be modified.Gravatar Jason Koenig2012-08-01
|
* Dafny: reverify if the refining method modifies the heap.Gravatar Jason Koenig2012-08-01
|
* Dafny: fixed bug where expressions were not replaced.Gravatar Jason Koenig2012-08-01
|
* Dafny: support opening modules into the local scopeGravatar Jason Koenig2012-07-30
|
* Dafny: removed allocated keyword, changed module import syntax. "opened" ↵Gravatar Jason Koenig2012-07-30
| | | | keyword is parsed but ignored.
* GPUVerify: add an option which controls whether to use smart predicationGravatar Peter Collingbourne2012-07-30
|
* VCGeneration: implement smart predicationGravatar Peter Collingbourne2012-07-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This predication algorithm is intended to reduce the complexity of predicated verification conditions by reducing the amount of predicated state and using only boolean algebra, as opposed to the previous algorithm which also uses integers. It assigns a unique predicate to every superblock, which is defined per Agrawal [1] except that superblocks are further partitioned such that either no element of the same superblock may be contained within a natural loop or each element of the superblock has the same innermost natural loop head. Predicates are assigned at the element of the superblock which dominates all others, and are reset to false at a loop head and at the start of a procedure in order to ensure correct execution for future iterations. When exiting a loop, all predicates corresponding to heads of exited loops are reset to false. The algorithm requires that every successor at every divergence point in the CFG contains assumes marked with an attribute (called ':partition') which a frontend uses to certify to the predicator that for each block, if each successor of that block contains an assume statement marked with :partition, exactly one of those assume statement's predicates will hold. The frontend we use for GPUVerify generates such attributes, and as such the new predicator is only used there, and the old predicator has been retained for Corral etc. [1] Hiralal Agrawal. Dominators, super blocks, and program coverage. In POPL '94, p25-34.
* Graph: make DomRelation and DominatorMap publicGravatar Peter Collingbourne2012-07-11
|
* BoogieDriver: correctly display time taken by prover if >60 secondsGravatar Peter Collingbourne2012-07-30
|
* Dafny: removed allocated, changed semantics of freshGravatar Jason Koenig2012-07-29
| | | | | -allocated(x) removed, as really only useful in old(...) -old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).
* Dafny: added structural refinement checkGravatar Jason Koenig2012-07-29
|
* MergeGravatar Unknown2012-07-20
|\
* | Implemented Houdini-based pointer analysis. Made inter-group race checking ↵Gravatar Unknown2012-07-20
| | | | | | | | default.
| * Dafny: fixed datatype GetHashCode() to make it consistent with Equals()Gravatar Jason Koenig2012-07-18
| |
| * Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵Gravatar Jason Koenig2012-07-17
| | | | | | | | parallel statements.
| * Dafny: compilation of abstract modules, including local definitions (as in ↵Gravatar Jason Koenig2012-07-17
| | | | | | | | | | | | | | module A as B = C) * * * Dafny: compilation of abstract modules, including local definitions (as in module A as B = C)
| * Dafny: allow implict self (as in "`field") in frame declarations.Gravatar Jason Koenig2012-07-16
|/
* MergeGravatar Unknown2012-07-17
|\
* | GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already ↵Gravatar Unknown2012-07-17
| | | | | | | | exist. Did some tidying up of old source code - removed functions related to Y and Z offsets which we do not use any more.
| * Dafny: update statements match up correctly in skeletons.Gravatar Jason Koenig2012-07-13
| |
| * Dafny: fixed bug in which old locals were not properly forbidden from being ↵Gravatar Jason Koenig2012-07-12
| | | | | | | | modified during refinement
| * Dafny: labeled (and unlabled) block statements are now matched during ↵Gravatar Jason Koenig2012-07-12
| | | | | | | | refinement.
| * Dafny: check that resolution successfully resolved all types, where appropriate.Gravatar Jason Koenig2012-07-12
| |
| * Dafny: restored soundness for refinement by disallowing certain updates and ↵Gravatar Jason Koenig2012-07-11
| | | | | | | | method calls
| * Dafny: fixed translation bug in maps with objects in the domain, added test caseGravatar Jason Koenig2012-07-11
| |
| * Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ↵Gravatar Jason Koenig2012-07-10
|/ | | | parallel syntax, other minor fixes
* MergeGravatar Unknown2012-07-10
|\
* | Read and write logging variables are now only generated if they do not ↵Gravatar Unknown2012-07-10
| | | | | | | | already exist.
| * Dafny: fixed bad mergeGravatar Rustan Leino2012-07-09
| |
| * Dafny: rebuilt parser/scanner after previous mergeGravatar Rustan Leino2012-07-09
| |
| * MergeGravatar Rustan Leino2012-07-09
| |\
| * | Dafny: More work on the coinduction principleGravatar Rustan Leino2012-07-09
| | |
| | * MergeGravatar Jason Koenig2012-07-09
| | |\
| | * | Dafny: added verification that replaced expressions are the same as the originalGravatar Jason Koenig2012-07-09
| | | |
| | * | Dafny: added named expressions and replacementGravatar Jason Koenig2012-07-09
| | | |
| | | * GPUVerify: merge blocks into predecessors before and after predicationGravatar Peter Collingbourne2012-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Because predication produces straight line control flow, merging after predication can dramatically reduce the number of blocks to 1 plus 2-3 per loop. We also merge before predication, which reduces VC complexity by reducing the number of possible values for cur.
| | | * VCGen: add MergeBlocksIntoPredecessors functionGravatar Peter Collingbourne2012-07-09
| | |/
| | * Dafny: types can now be qualified with full module pathsGravatar Jason Koenig2012-07-06
| | |
| | * Dafny: datatype constructors can be accessed across module boundaries.Gravatar Jason Koenig2012-07-06
| | |
| | * Dafny: fixed a crash in datatype argument resolutionGravatar Jason Koenig2012-07-05
| | |
| | * MergeGravatar Jason Koenig2012-07-05
| | |\
| | * | Dafny: Fixed bug in autocontracts where the post resolver was run even if ↵Gravatar Jason Koenig2012-07-05
| | | | | | | | | | | | | | | | there were resolution errors.
| | * | Dafny: disallow importing ghost modules into physical ones.Gravatar Jason Koenig2012-07-05
| | | |
| * | | MergeGravatar Rustan Leino2012-07-04
| |\ \ \ | | | |/ | | |/|
| | * | Made error trace generation (without labels) more general for stratifiedGravatar Unknown2012-07-04
| | |/ | | | | | | | | | inlining
| | * Dafny: added static members of _default to the module level scope, at low ↵Gravatar Jason Koenig2012-07-03
| | | | | | | | | | | | priority.
| | * MergeGravatar Jason Koenig2012-07-03
| |/| |/| |
| | * Dafny: added support for nested abstract modules, fixed some translation issuesGravatar Jason Koenig2012-07-03
| | |
| * | Dafny: removed old Substitute method (which has been replaced by a ↵Gravatar Rustan Leino2012-07-03
| | | | | | | | | | | | Substituter class)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-01 16:19:07 +0000