summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Dafny: Implemented abstract modulesGravatar Jason Koenig2012-06-26
|
* MergeGravatar Jason Koenig2012-06-19
|\
* | Dafny: disallow declare identifiers starting with underscore (_)Gravatar Jason Koenig2012-06-19
| | | | | | | | | | | | It is still possible to reference names containing an underscore, but it is not possible to make a variable, method, class, bound variable, type, or module name beginning with one.
* | Dafny: Added nested modulesGravatar Jason Koenig2012-06-19
| |
| * MergeGravatar qadeer2012-06-18
| |\
| | * Backed out changeset: 7c8e7338652bGravatar qadeer2012-06-18
| | |
| * | Fix line endingsGravatar Peter Collingbourne2012-06-18
| | |
| * | Move block predicator to VCGenerationGravatar Peter Collingbourne2012-06-18
| | |
| * | GPUVerify: block predicator: add a mode which disables procedure predicatesGravatar Peter Collingbourne2012-06-18
|/ / | | | | | | | | This mode also conditionalises if statements to avoid problems with recursion.
| * MergeGravatar qadeer2012-06-17
|/|
| * an experiment trying to get predication into BoogieGravatar qadeer2012-06-17
| |
* | Dafny: fixed parsing bug.Gravatar Jason Koenig2012-06-15
| |
* | GPUVerify: implement is-a-constant analysisGravatar Peter Collingbourne2012-06-15
|/ | | | | | | | | | | | | This analysis is used to generate race checking invariants for arbitrary (thread-level) constant offsets, in place of invariant generators for four specific constants (thread-id, global-id, 2D thread-id and 2D global-id) which are subsumed by the new analysis. The main motivation is to be able to recognise offsets used by word level accesses into byte arrays, which are formed from linear combinations of thread IDs and constants. This change allows us to remove the 2D and global size analyses, resulting in a 536-line net reduction in total code size.
* GPUVerify: revert ac36537a0eb8, as this is in fact a candidate invariant ↵Gravatar Peter Collingbourne2012-06-15
| | | | | | (e.g. consider a loop within a conditional) Pointed out by Ally.
* GPUVerify: when dualising assume and assert statements, emit two statements ↵Gravatar Peter Collingbourne2012-06-15
| | | | instead of a conjunction
* MergeGravatar Unknown2012-06-14
|\
* | Dafny: in compiler, respect C#'s different scoping rules and lack of support ↵Gravatar Unknown2012-06-14
| | | | | | | | for special characters in identifiers
* | MergeGravatar Unknown2012-06-14
|\ \
* | | Dafny: fixed a couple of compiler bugsGravatar Unknown2012-06-14
| | |
* | | Dafny: cleaned up test scripts a littleGravatar Unknown2012-06-14
| | |
| | * Inter-thread race checking implementation done.Gravatar Unknown2012-06-14
| | |
| | * Fix for structured regions.Gravatar Unknown2012-06-14
| | |
| | * Progress on inter-group race checkingGravatar Unknown2012-06-14
| | |
| | * MergeGravatar Unknown2012-06-14
| | |\ | | |/ | |/|
| | * Started work on inter-group race checking.Gravatar Unknown2012-06-14
| | |
| * | MergeGravatar Jason Koenig2012-06-13
| |\ \ | |/ / |/| |
| * | Dafny: allow parallel assignments to assign to the same LHS if the RHS match.Gravatar Jason Koenig2012-06-13
| | |
* | | MergeGravatar Unknown2012-06-13
|\| |
* | | Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to ↵Gravatar Unknown2012-06-13
| | | | | | | | | | | | check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
| * | MergeGravatar Jason Koenig2012-06-13
| |\ \
| * | | Dafny: liberalized equality to work when the types could possibly be the sameGravatar Jason Koenig2012-06-13
| | | | | | | | | | | | | | | | (i.e. a != b is allowed when a: array<int> and b: array<T>)
* | | | Dafny: added another version of the majority finding algorithm to the test suiteGravatar Unknown2012-06-12
|/ / /
| * / GPUVerify: the non-uniform loop invariant is not a candidate invariantGravatar Peter Collingbourne2012-06-12
|/ / | | | | | | Thanks to Ally for pointing this out.
* | MergeGravatar Unknown2012-06-12
|\ \
* | | Dafny: beefed up allocation axioms for boxes stored in fieldsGravatar Unknown2012-06-12
| | |
| * | deleted an unused classGravatar qadeer2012-06-12
| | |
| * | MergeGravatar qadeer2012-06-12
| |\ \ | |/ / |/| |
| * | refactoring in SIGravatar qadeer2012-06-12
| | |
* | | Dafny: allow types to be qualified with the name of the module that declares ↵Gravatar Unknown2012-06-11
| | | | | | | | | | | | them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member)
* | | Dafny: fixed bug in type cloning, as part of refinement machineryGravatar Unknown2012-06-11
| | |
* | | Dafny: removed support for the old keyword "unlimited" (all functions are ↵Gravatar Unknown2012-06-11
| | | | | | | | | | | | limited)
* | | GPUVerify: emit non-uniform loop candidate invariantGravatar Peter Collingbourne2012-06-11
| | |
* | | GPUVerify: emit "uniform loop" candidate invariantGravatar Peter Collingbourne2012-06-11
| | |
* | | GPUVerify: dualiser: preserve attributes of assert cmdGravatar Peter Collingbourne2012-06-11
| | | | | | | | | | | | This allows us to retain invariant tags.
* | | GPUVerify: factor out CreateCandidateInvariant from AddCandidateInvariantGravatar Peter Collingbourne2012-06-11
| | | | | | | | | | | | | | | This allows us to build candidate invariants in situations where we don't have a Region, such as the block predicator.
* | | GPUVerify: initialise invariantGenerationCounter in the constructor, rather ↵Gravatar Peter Collingbourne2012-06-11
| |/ |/| | | | | | | | | | | than in ComputeInvariant This allows us to emit invariants in places earlier than ComputeInvariant (such as the block predicator).
| * MergeGravatar qadeer2012-06-10
| |\ | |/ |/|
| * 1. changed new SI implemnetation so that it performs substitution for call sitesGravatar qadeer2012-06-10
| | | | | | | | 2. changed the block expression to be the negation of the disjunction of all outgoing edges
* | Dafny: added some test programsGravatar Rustan Leino2012-06-08
| |
* | Dafny/Boogie/BVD: made Dafny plug-in for BVD work againGravatar Rustan Leino2012-06-08
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 21:55:13 +0000