debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	GPUVerify: resolve barrier implementation in unstructured mode	Peter Collingbourne	2012-05-31
\| \| \| \| \|	Resolution of goto labels is required for the graph builder to work.
*	GPUVerify: teach analyses, dualiser and race instrumenter about assigns with ↵	Peter Collingbourne	2012-05-31
\| \| \| \|	multiple LHSs
*	GPUVerify: disable barrier divergence check in unstructured mode for now	Peter Collingbourne	2012-05-30
\|
*	GPUVerify: have shared state abstraction, race instrumenter reuse blocks	Peter Collingbourne	2012-05-30
\| \| \| \| \|	Since we do not update transfer commands, they would otherwise refer to old blocks.
*	GPUVerify: factor shared state abstraction for unstructured blocks	Peter Collingbourne	2012-05-29
\|
*	GPUVerify: mark new work-item constants as non-unique	Peter Collingbourne	2012-05-29
\|
*	GPUVerify: implement a set of BV operation constructors which insert a ↵	Peter Collingbourne	2012-05-25
\| \| \| \|	function declaration if missing
*	GPUVerify: declarations of barrier, work-item constants no longer required; ↵	Peter Collingbourne	2012-05-25
\| \| \| \|	GPUVerify will create them if not present
*	GPUVerify: add a MakeDual for unstructured blocks	Peter Collingbourne	2012-05-25
\|
*	GPUVerify: add block predicator	Peter Collingbourne	2012-05-25
\|
*	GPUVerify: add an /unstructured command line option	Peter Collingbourne	2012-05-25
\|
*	Significantly changed the way race checking is performed. Made eager race ↵	Unknown	2012-04-24
\| \| \| \|	checking and symmetry reduction default, and removed the option to turn these off - makes the code a lot cleaner.
*	Inference in GPUVerify now merges candidates for threads 1 and 2 into a ↵	Unknown	2012-04-10
\| \| \| \|	single conjunctive candidate.
*	Don't insert final barrier when eager race checking is enabled.	paulthomson	2012-04-09
\|
*	More accessed offset inference	Unknown	2012-04-09
\|
*	Refined assertion.	Unknown	2012-04-06
\|
*	Extended GPUVerify's candidate invariant generation to use thread id inference.	Unknown	2012-04-05
\|
*	Inference of thread ids complete.	Unknown	2012-04-05
\|
*	Thread id inference now generalised to infer other thread configuration ↵	Unknown	2012-04-05
\| \| \| \|	parameters.
*	Started generalising thread id inference	Unknown	2012-04-05
\|
*	GPUverify now automatically decides then to use adversarial abstraction.	Unknown	2012-04-05
\|
*	Added support for break and return.	Unknown	2012-04-03
\|
*	Fixed bug with GPUVerify precondition generation	Unknown	2012-03-30
\|
*	Improved invariant inference.	Unknown	2012-03-28
\|
*	Started adding another invariant generation analysis.	Unknown	2012-03-26
\|
*	Started on live variable analysis in GPUVerify	Unknown	2012-03-26
\|
*	Added "may be power of two" analysis.	Unknown	2012-03-25
\|
*	Added "may be tid" analysis.	Unknown	2012-03-24
\|
*	Using uniform expression analysis in GPUVerify - also did some major ↵	Unknown	2012-03-24
\| \| \| \|	refactoring to GPUVerify.
*	Added uniform expression analysis, and started using it to do less predication.	Unknown	2012-03-23
\|
*	Do not generate equality candidates for variables that are not in the mod set.	Unknown	2012-03-22
\|
*	Cleaned up some GPUVerify code.	Unknown	2012-03-22
\|
*	Added the option to let user determine whether or not GPUVerify should add ↵	Unknown	2012-03-19
\| \| \| \|	invariants checking equality between arrays.
*	Improved kernel precondition generation	Unknown	2012-03-17
\|
*	Race checking assertions are now added as invariants and pre/post conditions ↵	Unknown	2012-03-05
\| \| \| \|	by default. Also added a StructuredProgramVisitor class, to try to avoid code duplication. Changed Predicator to use this.
*	Support for __all and __at_most_one annotations	Unknown	2012-03-04
\|
*	More annotation support	Unknown	2012-03-04
\|
*	Support for access annotations.	Unknown	2012-03-01
\|
*	Adding support for annotations written in the OpenCL/CUDA kernels.	Unknown	2012-02-29
\|
*	Fixed compilation problems in GPUVerify	Unknown	2012-02-28
\|
*	Added support for invariants in GPUVerify input.	Unknown	2012-02-28
\|
*	Fix: Check for duplicate special constants (with attributes).	paulthomson	2012-02-09
\|
*	Support for language-specific thread ids.	Unknown	2012-02-07
\|
*	A few fixes to get GPUVerify working with OpenCL front-end.	Unknown	2011-12-15
\|
*	Some fixes to get GPUVerify close to working with OpenCL.	Unknown	2011-12-09
\|
*	Changed names of builtins to make them generic.	Unknown	2011-12-07
\|
*	Generating useful, and guarateed by construction, postconditions and loop ↵	Unknown	2011-11-21
\| \| \| \|	invariants for kenrel procedures.
*	Better support for race-checking contracts	Unknown	2011-11-16
\|
*	Some fixes for race checking contracts	Unknown	2011-11-15
\|
*	Refactoring, and work on race checking contracts	Unknown	2011-11-09
\|