summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* DafnyExtension: report out-of-time and out-of-memory errorsGravatar Rustan Leino2012-08-17
|
* DafnyExtension: toward some fixesGravatar Unknown2012-08-17
|
* DafnyExtension: simplified display of type names and field namesGravatar Unknown2012-08-17
|
* DafnyExtension: various improvementsGravatar Unknown2012-08-16
|
* Fixed bug where source location attributes are not being attached to a CHECKGravatar Unknown2012-08-16
| | | | call, and refactored code to avoid the duplication which caused this error.
* DafnyExtension: improvementsGravatar Rustan Leino2012-08-15
|
* DafnyExtension: do verification in a non-UI threadGravatar Rustan Leino2012-08-15
|
* DafnyExtension: fixed more missing cases for hover textsGravatar Unknown2012-08-15
|
* Dafny: fixed some bugs in the newly added DafnyExtension codeGravatar Unknown2012-08-15
|
* MergeGravatar Unknown2012-08-15
|\
* | Dafny: added Statement.SubExpressions getterGravatar Unknown2012-08-15
| | | | | | | | DafnyExtension: added hover text for identifiers
* | 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
| |
| * Boogie build succeededGravatar CodeplexBot2012-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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 14:49:50 +0000