Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | removed lazy inlining | 2012-04-28 | |
| | |||
* | Merge | 2012-04-27 | |
|\ | |||
* | | unsat core for houdini | 2012-04-27 | |
| | | |||
| * | Dafny: fixed unsoundness having to do with a function depending on the ↵ | 2012-04-27 | |
| | | | | | | | | allocation state | ||
| * | Dafny: added resolution tests cases for inductive datatypes | 2012-04-27 | |
| | | |||
| * | Merge | 2012-04-26 | |
| |\ | |/ |/| | |||
| * | Dafny: fixed bug that had omitted the computation of .DefaultCtor for some ↵ | 2012-04-26 | |
| | | | | | | | | inductive datatypes | ||
| * | Dafny: compile co-inductive datatypes | 2012-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 datatypes | 2012-04-25 | |
| | | |||
| * | Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵ | 2012-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) | ||
* | | Merge | 2012-04-24 | |
|\| | |||
* | | Started refactoring invariant generation rules. | 2012-04-24 | |
| | | |||
* | | Removed set encoding. | 2012-04-24 | |
| | | |||
* | | Significantly changed the way race checking is performed. Made eager race ↵ | 2012-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. | 2012-04-24 | |
| | | | | | | | | Don't use UNSAT core for the refinement step. | ||
| * | Merge | 2012-04-20 | |
| |\ | |/ |/| | |||
| * | Dafny: fixed bug (missing Boogie cast) in translation of induction over ↵ | 2012-04-20 | |
| | | | | | | | | generic datatypes instantiated with datatypes | ||
* | | removed BoogieDriver from solution | 2012-04-18 | |
| | | |||
* | | Boogie build succeeded | 2012-04-18 | |
| | | |||
* | | Merge | 2012-04-17 | |
|\ \ | |||
* | | | various changes for using unsat cores in Houdini | 2012-04-17 | |
| | | | |||
| * | | Add options to control the emission of free ensures for | 2012-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. | ||
| * | | Merge | 2012-04-15 | |
| |\ \ | |/ / |/| | | |||
| * | | Removed expression simplifier (actually just commented | 2012-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. | ||
* | | Merge | 2012-04-13 | |
|\ \ | |||
* | | | Made loop predicate invariant optionally generated. | 2012-04-13 | |
| | | | |||
| * | | Added functionality to "skip" procedures. Some cleanup. | 2012-04-12 | |
| |/ | |||
| * | Temp file added as one to ignore. | 2012-04-10 | |
| | | |||
| * | Merge | 2012-04-10 | |
| |\ | |/ |/| | |||
| * | Added "free ensures" to procedures encoding the allocatedness | 2012-04-10 | |
| | | | | | | | | of references. | ||
* | | Added invariant to predicated loops. | 2012-04-10 | |
| | | |||
* | | Minor fix to array control flow analysis. | 2012-04-10 | |
| | | |||
* | | Merge | 2012-04-10 | |
|\| | |||
* | | Inference in GPUVerify now merges candidates for threads 1 and 2 into a ↵ | 2012-04-10 | |
| | | | | | | | | single conjunctive candidate. | ||
| * | Merge | 2012-04-09 | |
| |\ | |/ |/| | |||
| * | Fix a lot of the translation of "op=" expressions | 2012-04-09 | |
| | | | | | | | | (like += or *=). | ||
* | | Don't insert final barrier when eager race checking is enabled. | 2012-04-09 | |
| | | |||
* | | Tweak to inference. | 2012-04-09 | |
| | | |||
* | | More accessed offset inference | 2012-04-09 | |
|/ | |||
* | Refined assertion. | 2012-04-06 | |
| | |||
* | Tuned candidate generation. | 2012-04-06 | |
| | |||
* | Extended GPUVerify's candidate invariant generation to use thread id inference. | 2012-04-05 | |
| | |||
* | Inference of thread ids complete. | 2012-04-05 | |
| | |||
* | Thread id inference now generalised to infer other thread configuration ↵ | 2012-04-05 | |
| | | | | parameters. | ||
* | Thread id inference now generalised to three dimensions. | 2012-04-05 | |
| | |||
* | Started generalising thread id inference | 2012-04-05 | |
| | |||
* | Merge | 2012-04-05 | |
|\ | |||
* | | GPUverify now automatically decides then to use adversarial abstraction. | 2012-04-05 | |
| | | |||
| * | Fixed bug with triply nested maps and polymorphism (reported as Item # 10218). | 2012-04-04 | |
| | | |||
| * | small fix | 2012-04-04 | |
| | | | | | | | | added regressions |