debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Fixed bug with uniformity analysis for havoc. Allowed barrier invariants to	Unknown	2012-09-28
\| \| \| \| \|	support a more expressive class of expressions. Refactored thread id creation functions.
*	Barrier invariants can now refer to local variables that are uniform.	Unknown	2012-09-26
\|
*	Fixed issue with uniformity analysis and block merging. Uniformity analysis	Unknown	2012-09-24
\| \| \| \|	now enabled by default.
*	Support for barrier invariants.	Unknown	2012-09-24
\|
*	Fixed a bug with empty big blocks.	Unknown	2012-09-21
\|
*	Added support for invariants about shared state.	Unknown	2012-09-21
\| \| \| \| \| \|	Reworked implementation of barriers. Started on support for barrier invariants.
*	When uniformity analysis is disabled, no procedures (even the kernel entry	Unknown	2012-09-19
\| \| \| \| \|	point) will be regarded as uniform. This simplification avoids various edge cases.
*	Uniformity analysis. Patch by Peter Collingbourne.	Unknown	2012-09-18
\|
*	Dualisation modified so that global arrays are not dualised, and group-shared	Unknown	2012-09-18
\| \| \| \| \| \| \| \| \|	arrays are turned into 2D maps with first index type bool. Thread 1 always indexes into "true", while threads 2 indexes into "samegroup" (a formula which is true iff threads 1 and 2 are in the same group). Thus if the threads are in different groups they operate on different shared arrays, but if they are in the same group they operate on the same shared array. This paves the way for implementing support for barrier invariants.
*	During dualisation,	Unknown	2012-09-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	x := y; now becomes x$1 := y$1; x$2 := y$2; instead of x$1, x$2 := y$1, y$2; This is to make way for further changes.
*	Added creation of source variable pre- and post- conditions.	Egor Kyshtymov	2012-09-16
\| \| \| \| \|	Changed style of error messages. Cleaned up error reporting code.
*	Moved point at which preprocessed output is shown.	Unknown	2012-08-31
\|
*	Shared state is now properly abstracted in requires clauses.	Unknown	2012-08-31
\|
*	Barriers now handled uniformly via bugle_barrier.	Unknown	2012-08-30
\| \| \| \| \| \| \| \| \| \| \|	Improved loop invariant inference so that procedure formal parameters are treated as constants. (This involved fixing a bug where a Formal was being dualised to a LocalVariable.) Fixed problem in GPUVerifyBoogieDriver where source location information was being looked for via a file name, rather than a full path. Cleaned up some code in GPUVerifyBoogieDriver.
*	A small fix in variable definition analysis.	Unknown	2012-08-29
\|
*	Added generation of invariants to restrict source location to sensible values.	Egor Kyshtymov	2012-08-28
\| \| \| \| \|	Refactored Make...Variable() and FindOrCreate...Variable() functions to take a variable name as a parameter rather than the variable itself.
*	Fixed problem where SOURCE variables were not being generated.	Unknown	2012-08-20
\|
*	Added functionality for race error reporting.	Egor Kyshtymov	2012-08-20
\|
*	Fixed bug where source location attributes are not being attached to a CHECK	Unknown	2012-08-16
\| \| \| \|	call, and refactored code to avoid the duplication which caused this error.
*	Separated race checking into logging and checking calls. This simplifies	Unknown	2012-08-14
\| \| \| \|	error reporting.
*	Removed some dud code for handling nested maps, which we no longer support.	Unknown	2012-08-13
\|
*	Some more code cleanup related to removal of the "divided" option.	Unknown	2012-08-13
\|
*	Removed code related to "divided" option.	Unknown	2012-08-13
\|
*	Barrier divergence checking now achieved via precondition.	Unknown	2012-08-13
\| \| \| \| \| \|	Race checking assertions contain tags to identify them. Attributes are passed correctly through the dualisation process.
*	Unstructured and smart predication are now default options for GPUVerify.	Unknown	2012-08-09
\| \| \| \| \| \|	The executable produced by building the project is now GPUVerifyVCGen. Refactored the way "other" functions are handled to make this more easily extensible.
*	Revised candidate invariant generation for barrier divergence checking.	Unknown	2012-08-07
\|
*	Smart block predicator: drop the unused createCandidateInvariants parameter	Peter Collingbourne	2012-08-06
\|
*	GPUVerify: add an option which controls whether to use smart predication	Peter Collingbourne	2012-07-30
\|
*	Implemented Houdini-based pointer analysis. Made inter-group race checking ↵	Unknown	2012-07-20
\| \| \| \|	default.
*	GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already ↵	Unknown	2012-07-17
\| \| \| \|	exist. Did some tidying up of old source code - removed functions related to Y and Z offsets which we do not use any more.
*	Merge	Unknown	2012-07-10
\|\
* \|	Read and write logging variables are now only generated if they do not ↵	Unknown	2012-07-10
\| \| \| \| \| \| \| \|	already exist.
\| *	GPUVerify: merge blocks into predecessors before and after predication	Peter Collingbourne	2012-07-09
\|/ \| \| \| \| \| \|	Because predication produces straight line control flow, merging after predication can dramatically reduce the number of blocks to 1 plus 2-3 per loop. We also merge before predication, which reduces VC complexity by reducing the number of possible values for cur.
*	Worked on cross-thread annotations.	Unknown	2012-07-03
\|
*	Reinstate GPUVerify files	Peter Collingbourne	2012-07-02
\|
*	Merge	Unknown	2012-07-02
\|\
* \|	Started adding support for annotation intrinsics for unstructured programs.	Unknown	2012-07-02
\| \|
\| *	Merge	Jason Koenig	2012-06-28
\| \|\ \| \|/ \|/\|
\| *	Dafny: Merge	Jason Koenig	2012-06-27
\| \|\
* \| \|	GPUVerify: modify the variable definition analysis to track and reject ↵	Peter Collingbourne	2012-06-27
\| \|/ \|/\| \| \| \| \| \| \| \| \|	self-referential definitions Fixes Bugzilla bug #66.
* \|	GPUVerify: when building offset predicates, skip unsubstitutable offsets	Peter Collingbourne	2012-06-27
\| \| \| \| \| \| \| \|	Fixes Bugzilla bug #65.
* \|	GPUVerify: use original expression for undefined variables	Peter Collingbourne	2012-06-27
\| \| \| \| \| \| \| \|	Fixes Bugzilla bug #64.
* \|	GPUVerify: implement generic reduced strength analysis for loop counters	Peter Collingbourne	2012-06-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	All counters which we are able to infer facts about now receive a candidate invariant _before_ predication, dualisation etc. This is probably a more natural place to insert such invariants, and means that they are also subject to predication etc. without us having to do anything. Also, kill the id plus constant analyses, which are no longer used.
* \|	GPUVerify: fix UnstructuredRegion.CmdsChildRegions	Peter Collingbourne	2012-06-26
\| \|
* \|	Reinstated support for barrier flags.	Unknown	2012-06-27
\| \|
* \|	Undo bad merge.	afd	2012-06-27
\| \|
* \|	Merge	Unknown	2012-06-26
\|\ \
* \| \|	Added support for barrier flags.	Unknown	2012-06-26
\| \| \|
* \| \|	Merge	Unknown	2012-06-25
\|\ \ \
\| \| * \|	GPUVerify: factor all offset predicate handling code into a central location	Peter Collingbourne	2012-06-25
\| \| \| \|