summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* MergeGravatar Rustan Leino2012-05-01
|\
* | Dafny: print inductive datatypesGravatar Rustan Leino2012-05-01
* | Dafny: added support for co-recursive callsGravatar Rustan Leino2012-05-01
| * Boogie build succeededGravatar CodeplexBot2012-05-01
| * log file fixGravatar qadeer2012-04-30
| * Update to match the new model printing formatGravatar Michal Moskal2012-04-30
| * UseLabels=false when stratified inline is onGravatar qadeer2012-04-29
| * MergeGravatar qadeer2012-04-29
| |\ | |/ |/|
| * clean up in stratified inliningGravatar qadeer2012-04-29
* | Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2012-04-29
|/
* eliminated class ErrorModelGravatar qadeer2012-04-28
* removed proccopybounding codeGravatar qadeer2012-04-28
* eliminated LazyInliningInfoGravatar qadeer2012-04-28
* removed the lazy inline test directoryGravatar qadeer2012-04-28
* MergeGravatar qadeer2012-04-28
|\
* | removed lazy inliningGravatar qadeer2012-04-28
| * Boogie build succeededGravatar CodeplexBot2012-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 alloca...Gravatar Unknown2012-04-27
| * 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 in...Gravatar Unknown2012-04-26
| * Dafny: compile co-inductive datatypesGravatar Unknown2012-04-26
| * Dafny: rudimentary translation into Boogie of co-inductive datatypesGravatar Unknown2012-04-25
| * Dafny: fixed resolution bug for inductive datatypes (previous check did not h...Gravatar Unknown2012-04-25
* | 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 ch...Gravatar Unknown2012-04-24
| * Added test to stratified inlining.Gravatar Unknown2012-04-24
| * MergeGravatar Unknown2012-04-20
| |\ | |/ |/|
| * Dafny: fixed bug (missing Boogie cast) in translation of induction over gener...Gravatar Unknown2012-04-20
* | 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
| * | MergeGravatar Unknown2012-04-15
| |\ \ | |/ / |/| |
| * | Removed expression simplifier (actually just commentedGravatar Unknown2012-04-15
| |/
* | 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
* | 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 singl...Gravatar Unknown2012-04-10