| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Dafny: allow parallel assignments to assign to the same LHS if the RHS match. |  Jason Koenig | 2012-06-13 |
| | | |||
| * | Merge | Jason Koenig | 2012-06-13 |
| |\ | |||
| * | | Dafny: liberalized equality to work when the types could possibly be the same | Jason Koenig | 2012-06-13 |
| | | | | | | | | | (i.e. a != b is allowed when a: array<int> and b: array<T>) | ||
| | * | GPUVerify: the non-uniform loop invariant is not a candidate invariant |  Peter Collingbourne | 2012-06-12 |
| |/ | | | | Thanks to Ally for pointing this out. | ||
| * | Merge |  Unknown | 2012-06-12 |
| |\ | |||
| * | | Dafny: beefed up allocation axioms for boxes stored in fields | Unknown | 2012-06-12 |
| | | | |||
| | * | deleted an unused class |  qadeer | 2012-06-12 |
| | | | |||
| | * | Merge | qadeer | 2012-06-12 |
| | |\ | |/ |/| | |||
| | * | refactoring in SI | qadeer | 2012-06-12 |
| | | | |||
| * | | Dafny: allow types to be qualified with the name of the module that declares ↵ | Unknown | 2012-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 machinery | Unknown | 2012-06-11 |
| | | | |||
| * | | Dafny: removed support for the old keyword "unlimited" (all functions are ↵ | Unknown | 2012-06-11 |
| | | | | | | | | | limited) | ||
| * | | GPUVerify: emit non-uniform loop candidate invariant | Peter Collingbourne | 2012-06-11 |
| | | | |||
| * | | GPUVerify: emit "uniform loop" candidate invariant | Peter Collingbourne | 2012-06-11 |
| | | | |||
| * | | GPUVerify: dualiser: preserve attributes of assert cmd | Peter Collingbourne | 2012-06-11 |
| | | | | | | | | | This allows us to retain invariant tags. | ||
| * | | GPUVerify: factor out CreateCandidateInvariant from AddCandidateInvariant | Peter Collingbourne | 2012-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 ↵ | Peter Collingbourne | 2012-06-11 |
| | | | | | | | | | | | | | | | than in ComputeInvariant This allows us to emit invariants in places earlier than ComputeInvariant (such as the block predicator). | ||
| | * | Merge | qadeer | 2012-06-10 |
| | |\ | |/ |/| | |||
| | * | 1. changed new SI implemnetation so that it performs substitution for call sites | qadeer | 2012-06-10 |
| | | | | | | | | | 2. changed the block expression to be the negation of the disjunction of all outgoing edges | ||
| * | | Dafny: added some test programs |  Rustan Leino | 2012-06-08 |
| | | | |||
| * | | Dafny/Boogie/BVD: made Dafny plug-in for BVD work again | Rustan Leino | 2012-06-08 |
| | | | |||
| * | | GPUVerify: teach the array control flow analyser to handle unstructured programs | Peter Collingbourne | 2012-06-08 |
| | | | |||
| * | | GPUVerify: if one input file is supplied, choose output file name more ↵ | Peter Collingbourne | 2012-06-08 |
| | | | | | | | | | | | | | | | intelligently Specifically, if the input file's extension is not ".bpl", use its name (without extension) plus ".bpl" as the output file name. | ||
| * | | GPUVerify: fix line endings | Peter Collingbourne | 2012-06-08 |
| | | | |||
| * | | Chalice build succeeded | CodeplexBot | 2012-06-08 |
| |/ | |||
| * | Merge | qadeer | 2012-06-07 |
| |\ | |||
| * | | final (hopefully) fix to new SI | qadeer | 2012-06-07 |
| | | | |||
| | * | Boogie build succeeded | CodeplexBot | 2012-06-08 |
| |/ | |||
| * | testing a fix in SI | qadeer | 2012-06-07 |
| | | | | | | also changing back the output path in BoogieDriver also disabling z3api for now since it does not build | ||
| * | Merging again |  Ken McMillan | 2012-06-07 |
| |\ | |||
| * | | GPUVerify: have StripThreadIdentifiers deal properly with identifiers ↵ | Peter Collingbourne | 2012-06-07 |
| | | | | | | | | | containing a '$' | ||
| * | | GPUVerify: block predicator: use the name '_P' for the procedure predicate ↵ | Peter Collingbourne | 2012-06-07 |
| | | | | | | | | | for consistency with the structured predicator | ||
| * | | GPUVerify: re-introduce the non-divergence check in unstructured mode | Peter Collingbourne | 2012-06-07 |
| | | | | | | | | | This is OK now that we have assume stealing. | ||
| * | | GPUVerify: emit assumes for backedges | Peter Collingbourne | 2012-06-07 |
| | | | | | | | | | | | | | Specifically, have the predicator emit backedge assumes with a :backedge attribute, and have the dualiser recognise such assumes and create an OR expression instead of an AND expression. | ||
| * | | GPUVerify: refactor candidate invariant generators and analyses to use regions | Peter Collingbourne | 2012-06-07 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main goal of this change is to make the candidate invariant generation code and various analyses capable of handling both structured and unstructured programs. This is achieved using a high level abstraction of "regions" -- a region may either be a "root region" representing the entire implementation, or a natural loop within that implementation. Note that this is a subset to the term's meaning in the context of compilers, in which regions are also used for conditional control flow. Each region consists of a set of commands and a set of child regions. This change also has the side effect of eliminating a large amount of boilerplate code -- its net effect is to reduce the number of lines of code by 88. | ||
| * | | Automatic merge. | stefanheule | 2012-06-07 |
| |\ \ | |||
| * | | | Chalice: Remove IsGoodState as it is not needed and causes problems in ↵ | stefanheule | 2012-06-07 |
| | | | | | | | | | | | | | certain cases. | ||
| | | * | Trying to merge with recent changes, failing. | Ken McMillan | 2012-06-05 |
| | | |\ | |||
| | | | * | Some changes to support expanded use of z3api. | Ken McMillan | 2012-06-05 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after). | ||
| | * | | | GPUVerify: recognise offsets in forms other than that produced by the old ↵ | Peter Collingbourne | 2012-06-01 |
| | | | | | | | | | | | | | | | | | frontend | ||
| | * | | | GPUVerify: have dualiser reuse blocks | Peter Collingbourne | 2012-06-07 |
| | | | | | |||
| | * | | | GPUVerify: add newly created barrier procedures to resolution context | Peter Collingbourne | 2012-06-07 |
| | | | | | |||
| | * | | | Merge | Jason Koenig | 2012-06-06 |
| | |\ \ \ | |||
| | * | | | | Dafny: change labels to use a generic singly linked list | Jason Koenig | 2012-06-06 |
| | | | | | | |||
| | | * | | | GPUVerify: fix bug which caused us to log accesses at the end of the block, ↵ | Peter Collingbourne | 2012-06-06 |
| | |/ / / | | | | | | | | | | | | | rather than the appropriate place | ||
| | * | | | Boogie: add /printCFG command line option, which prints each ↵ | Peter Collingbourne | 2012-06-06 |
| | | | | | | | | | | | | | | | | | implementation's CFG in Graphviz format | ||
| | * | | | Bug fix with mvInfo during VCGen | akashlal | 2012-06-06 |
| | | | | | |||
| | * | | | update to SI | qadeer | 2012-06-04 |
| | |/ / | |||
| | * | | Merge | qadeer | 2012-06-04 |
| | |\ \ | |||
| | * | | | moved class Macro to Absy | qadeer | 2012-06-04 |
| | | | | | | | | | | | | | | | | | | | | | cleanup up DefineMacro Changed SI to use macros for reach info | ||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |