summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* removed lazy inliningGravatar qadeer2012-04-28
|
* MergeGravatar qadeer2012-04-27
|\
* | unsat core for houdiniGravatar qadeer2012-04-27
| |
| * Dafny: fixed unsoundness having to do with a function depending on the ↵Gravatar Unknown2012-04-27
| | | | | | | | allocation state
| * Dafny: added resolution tests cases for inductive datatypesGravatar Unknown2012-04-27
| |
| * MergeGravatar Unknown2012-04-26
| |\ | |/ |/|
| * Dafny: fixed bug that had omitted the computation of .DefaultCtor for some ↵Gravatar Unknown2012-04-26
| | | | | | | | inductive datatypes
| * Dafny: compile co-inductive datatypesGravatar Unknown2012-04-26
| | | | | | | | Dafny: for inductive datatypes, cache any default value computed and also produce slightly tidier target code
| * Dafny: rudimentary translation into Boogie of co-inductive datatypesGravatar Unknown2012-04-25
| |
| * Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵Gravatar Unknown2012-04-25
| | | | | | | | | | | | | | handle generic datatypes correctly) Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now)
* | MergeGravatar Unknown2012-04-24
|\|
* | Started refactoring invariant generation rules.Gravatar Unknown2012-04-24
| |
* | Removed set encoding.Gravatar Unknown2012-04-24
| |
* | Significantly changed the way race checking is performed. Made eager race ↵Gravatar Unknown2012-04-24
| | | | | | | | checking and symmetry reduction default, and removed the option to turn these off - makes the code a lot cleaner.
| * Added test to stratified inlining.Gravatar Unknown2012-04-24
| | | | | | | | Don't use UNSAT core for the refinement step.
| * MergeGravatar Unknown2012-04-20
| |\ | |/ |/|
| * Dafny: fixed bug (missing Boogie cast) in translation of induction over ↵Gravatar Unknown2012-04-20
| | | | | | | | generic datatypes instantiated with datatypes
* | removed BoogieDriver from solutionGravatar qadeer2012-04-18
| |
* | Boogie build succeededGravatar CodeplexBot2012-04-18
| |
* | MergeGravatar qadeer2012-04-17
|\ \
* | | various changes for using unsat cores in HoudiniGravatar qadeer2012-04-17
| | |
| * | Add options to control the emission of free ensures forGravatar Unknown2012-04-16
| | | | | | | | | | | | | | | | | | heap monotonicity (and allocatedness of references returned from a method) as well as the assert/assume checks that are generated for every object dereference.
| * | MergeGravatar Unknown2012-04-15
| |\ \ | |/ / |/| |
| * | Removed expression simplifier (actually just commentedGravatar Unknown2012-04-15
| |/ | | | | | | | | | | | | it out for now) and used a simpler scheme for always assigning compound bound expressions to a local. Added the ability to assert/assume that an object is non-null before dereferencing it.
* | MergeGravatar Unknown2012-04-13
|\ \
* | | Made loop predicate invariant optionally generated.Gravatar Unknown2012-04-13
| | |
| * | Added functionality to "skip" procedures. Some cleanup.Gravatar akashlal2012-04-12
| |/
| * Temp file added as one to ignore.Gravatar Unknown2012-04-10
| |
| * MergeGravatar Unknown2012-04-10
| |\ | |/ |/|
| * Added "free ensures" to procedures encoding the allocatednessGravatar Unknown2012-04-10
| | | | | | | | of references.
* | Added invariant to predicated loops.Gravatar Unknown2012-04-10
| |
* | Minor fix to array control flow analysis.Gravatar Unknown2012-04-10
| |
* | MergeGravatar Unknown2012-04-10
|\|
* | Inference in GPUVerify now merges candidates for threads 1 and 2 into a ↵Gravatar Unknown2012-04-10
| | | | | | | | single conjunctive candidate.
| * MergeGravatar Unknown2012-04-09
| |\ | |/ |/|
| * Fix a lot of the translation of "op=" expressionsGravatar Unknown2012-04-09
| | | | | | | | (like += or *=).
* | Don't insert final barrier when eager race checking is enabled.Gravatar paulthomson2012-04-09
| |
* | Tweak to inference.Gravatar Unknown2012-04-09
| |
* | More accessed offset inferenceGravatar Unknown2012-04-09
|/
* Refined assertion.Gravatar Unknown2012-04-06
|
* Tuned candidate generation.Gravatar Unknown2012-04-06
|
* Extended GPUVerify's candidate invariant generation to use thread id inference.Gravatar Unknown2012-04-05
|
* Inference of thread ids complete.Gravatar Unknown2012-04-05
|
* Thread id inference now generalised to infer other thread configuration ↵Gravatar Unknown2012-04-05
| | | | parameters.
* Thread id inference now generalised to three dimensions.Gravatar Unknown2012-04-05
|
* Started generalising thread id inferenceGravatar Unknown2012-04-05
|
* MergeGravatar Unknown2012-04-05
|\
* | GPUverify now automatically decides then to use adversarial abstraction.Gravatar Unknown2012-04-05
| |
| * Fixed bug with triply nested maps and polymorphism (reported as Item # 10218).Gravatar Unknown2012-04-04
| |
| * small fixGravatar qadeer2012-04-04
| | | | | | | | added regressions