Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | 2012-08-13 | |
|\ | |||
* | | Barrier divergence checking now achieved via precondition. | 2012-08-13 | |
| | | | | | | | | | | | | Race checking assertions contain tags to identify them. Attributes are passed correctly through the dualisation process. | ||
| * | Dafny: internal renaming | 2012-08-10 | |
| | | |||
| * | Dafny: added heuristics for finding witnesses in assign-such-that checking | 2012-08-10 | |
| | | |||
| * | DafnyExtension: hide execution-trace output, show split-expr related error ↵ | 2012-08-10 | |
| | | | | | | | | locations, set a 10-second timeout | ||
| * | Dafny: added MonotonicHeapstate refinement example | 2012-08-09 | |
| | | |||
| * | Dafny: fixed parser crash | 2012-08-09 | |
|/ | |||
* | Merge | 2012-08-09 | |
|\ | |||
* | | Unstructured and smart predication are now default options for GPUVerify. | 2012-08-09 | |
| | | | | | | | | | | | | The executable produced by building the project is now GPUVerifyVCGen. Refactored the way "other" functions are handled to make this more easily extensible. | ||
| * | DafnyExtension: improvements | 2012-08-08 | |
| | | |||
| * | DafnyExtension: fixed build issues; added support for some refinement features | 2012-08-08 | |
| | | |||
| * | Merge | 2012-08-08 | |
| |\ | |||
| * | | Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and ↵ | 2012-08-08 | |
| | | | | | | | | | | | | visually indicates a non-verified buffer | ||
* | | | Merge | 2012-08-07 | |
|\ \ \ | | |/ | |/| | |||
* | | | Revised candidate invariant generation for barrier divergence checking. | 2012-08-07 | |
| | | | |||
| * | | Houdini: recognise candidates of the form (p => (q => (... => (e => phi)))) ↵ | 2012-08-07 | |
|/ / | | | | | | | where e existential | ||
* | | Smart block predicator: track parents, and use to emit the invariant that if ↵ | 2012-08-06 | |
| | | | | | | | | a loop is enabled then so is its parent | ||
* | | Smart block predicator: move *Map from parameters to fields | 2012-08-06 | |
| | | |||
* | | Smart block predicator: drop the unused createCandidateInvariants parameter | 2012-08-06 | |
| | | |||
* | | Boogie build succeeded, 3 test(s) failed | 2012-08-04 | |
| | | |||
* | | Dafny: corrected comment | 2012-08-03 | |
| | | |||
* | | Core: attach :partition to assumes generated from structured ifs and whiles | 2012-08-03 | |
| | | |||
| * | Merge | 2012-08-02 | |
| |\ | |/ |/| | |||
| * | Dafny VS Extension: edited to make it build with new AST types, fixed some ↵ | 2012-08-02 | |
| | | | | | | | | bugs, added a temporary progress indicator | ||
* | | Dafny: fixed bug in reverifying allowing old locals to be modified. | 2012-08-01 | |
| | | |||
* | | Dafny: reverify if the refining method modifies the heap. | 2012-08-01 | |
| | | |||
* | | Dafny: fixed bug where expressions were not replaced. | 2012-08-01 | |
| | | |||
* | | Fix a bug when static fields are used in as operands for ++ or --. | 2012-07-31 | |
| | | |||
* | | Add an option to model exceptional control flow or not. When it is false: | 2012-07-31 | |
|/ | | | | | | method calls are not followed by a test to see if an exception was thrown "throw e" is translated as "assume false" "try S catch C finally F" is translated as "S; F" | ||
* | Dafny: support opening modules into the local scope | 2012-07-30 | |
| | |||
* | Dafny: removed allocated keyword, changed module import syntax. "opened" ↵ | 2012-07-30 | |
| | | | | keyword is parsed but ignored. | ||
* | Dafny: updated test suite to new syntax | 2012-07-30 | |
| | |||
* | GPUVerify: add an option which controls whether to use smart predication | 2012-07-30 | |
| | |||
* | VCGeneration: implement smart predication | 2012-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 public | 2012-07-11 | |
| | |||
* | BoogieDriver: correctly display time taken by prover if >60 seconds | 2012-07-30 | |
| | |||
* | Dafny: removed allocated, changed semantics of fresh | 2012-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 check | 2012-07-29 | |
| | |||
* | Merge | 2012-07-20 | |
|\ | |||
* | | Implemented Houdini-based pointer analysis. Made inter-group race checking ↵ | 2012-07-20 | |
| | | | | | | | | default. | ||
| * | Dafny: fixed datatype GetHashCode() to make it consistent with Equals() | 2012-07-18 | |
| | | |||
| * | Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵ | 2012-07-17 | |
| | | | | | | | | parallel statements. | ||
| * | Dafny: compilation of abstract modules, including local definitions (as in ↵ | 2012-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. | 2012-07-16 | |
|/ | |||
* | Merge | 2012-07-17 | |
|\ | |||
* | | GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already ↵ | 2012-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. | 2012-07-13 | |
| | | |||
| * | Dafny: fixed bug in which old locals were not properly forbidden from being ↵ | 2012-07-12 | |
| | | | | | | | | modified during refinement | ||
| * | Dafny: labeled (and unlabled) block statements are now matched during ↵ | 2012-07-12 | |
| | | | | | | | | refinement. | ||
| * | Dafny: check that resolution successfully resolved all types, where appropriate. | 2012-07-12 | |
| | |