summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
* 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
| * MergeGravatar Unknown2012-04-09
| |\ | |/ |/|
| * Fix a lot of the translation of "op=" expressionsGravatar Unknown2012-04-09
* | 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 param...Gravatar Unknown2012-04-05
* 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
| * MergeGravatar qadeer2012-04-03
| |\ | |/ |/|
| * added nonUniformUnfolding optionGravatar qadeer2012-04-03
* | Fixed bug with handling of return in GPUVerify.Gravatar Unknown2012-04-03
* | MergeGravatar Unknown2012-04-03
|\ \
* | | Added support for break and return.Gravatar Unknown2012-04-03
| | * deleted the option UseUnsatCoreForInliningGravatar qadeer2012-04-02
| | * MergeGravatar qadeer2012-04-01
| | |\ | | |/ | |/|
| | * commented out SuperAwesomeMethodGravatar qadeer2012-04-01
| * | bug fix for previous refactoringGravatar Unknown2012-04-02
| | * MergeGravatar qadeer2012-04-01
| | |\ | | |/ | |/|
| | * partial work on non-uniform loop unrollingGravatar qadeer2012-04-01
| * | Refactored CheckAssumptions APIGravatar Unknown2012-04-02
| |/
| * Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2012-03-30
|/|
| * Changed the BCT solution so it uses the CodePlex version of CCI (insteadGravatar Mike Barnett2012-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-01 02:52:46 +0000