summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Dafny: added Statement.SubExpressions getterGravatar Unknown2012-08-15
| | | | DafnyExtension: added hover text for identifiers
* Dafny: removed the defunct "havoc" keyword from various source-code highlightersGravatar Unknown2012-08-15
|
* MergeGravatar Unknown2012-08-14
|\
* | Dafny emacs mode: changed a menu name (Does anyone ever use this menu anyhow?)Gravatar Unknown2012-08-14
| |
* | Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension ↵Gravatar Unknown2012-08-14
| | | | | | | | crashing after certain deletes)
| * Also updated test15Gravatar Rustan Leino2012-08-14
| |
| * Update test suite for commit 8a59fbb7ee34.Gravatar Peter Collingbourne2012-08-14
| |
| * Added GPUVerifyBoogieDriver project.Gravatar Unknown2012-08-14
| | | | | | | | Contributed by Egor Kyshtymov.
| * Separated race checking into logging and checking calls. This simplifiesGravatar Unknown2012-08-14
| | | | | | | | error reporting.
| * Removed some dud code for handling nested maps, which we no longer support.Gravatar Unknown2012-08-13
| |
| * Some more code cleanup related to removal of the "divided" option.Gravatar Unknown2012-08-13
| |
| * Removed code related to "divided" option.Gravatar Unknown2012-08-13
|/
* MergeGravatar Unknown2012-08-13
|\
* | Barrier divergence checking now achieved via precondition.Gravatar Unknown2012-08-13
| | | | | | | | | | | | Race checking assertions contain tags to identify them. Attributes are passed correctly through the dualisation process.
| * Dafny: internal renamingGravatar Unknown2012-08-10
| |
| * Dafny: added heuristics for finding witnesses in assign-such-that checkingGravatar Unknown2012-08-10
| |
| * DafnyExtension: hide execution-trace output, show split-expr related error ↵Gravatar Rustan Leino2012-08-10
| | | | | | | | locations, set a 10-second timeout
| * Dafny: added MonotonicHeapstate refinement exampleGravatar Unknown2012-08-09
| |
| * Dafny: fixed parser crashGravatar Unknown2012-08-09
|/
* MergeGravatar Unknown2012-08-09
|\
* | Unstructured and smart predication are now default options for GPUVerify.Gravatar Unknown2012-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: improvementsGravatar Rustan Leino2012-08-08
| |
| * DafnyExtension: fixed build issues; added support for some refinement featuresGravatar Rustan Leino2012-08-08
| |
| * MergeGravatar Unknown2012-08-08
| |\
| * | Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and ↵Gravatar Unknown2012-08-08
| | | | | | | | | | | | visually indicates a non-verified buffer
* | | MergeGravatar Unknown2012-08-07
|\ \ \ | | |/ | |/|
* | | Revised candidate invariant generation for barrier divergence checking.Gravatar Unknown2012-08-07
| | |
| * | Houdini: recognise candidates of the form (p => (q => (... => (e => phi)))) ↵Gravatar Peter Collingbourne2012-08-07
|/ / | | | | | | where e existential
* | Smart block predicator: track parents, and use to emit the invariant that if ↵Gravatar Peter Collingbourne2012-08-06
| | | | | | | | a loop is enabled then so is its parent
* | Smart block predicator: move *Map from parameters to fieldsGravatar Peter Collingbourne2012-08-06
| |
* | Smart block predicator: drop the unused createCandidateInvariants parameterGravatar Peter Collingbourne2012-08-06
| |
* | Boogie build succeeded, 3 test(s) failedGravatar CodeplexBot2012-08-04
| |
* | Dafny: corrected commentGravatar Jason Koenig2012-08-03
| |
* | Core: attach :partition to assumes generated from structured ifs and whilesGravatar Peter Collingbourne2012-08-03
| |
| * MergeGravatar Unknown2012-08-02
| |\ | |/ |/|
| * Dafny VS Extension: edited to make it build with new AST types, fixed some ↵Gravatar Unknown2012-08-02
| | | | | | | | bugs, added a temporary progress indicator
* | 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
| |
* | Fix a bug when static fields are used in as operands for ++ or --.Gravatar Unknown2012-07-31
| |
* | Add an option to model exceptional control flow or not. When it is false:Gravatar Unknown2012-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 scopeGravatar Jason Koenig2012-07-30
|
* Dafny: removed allocated keyword, changed module import syntax. "opened" ↵Gravatar Jason Koenig2012-07-30
| | | | keyword is parsed but ignored.
* Dafny: updated test suite to new syntaxGravatar Jason Koenig2012-07-30
|
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 01:01:53 +0000