debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	GPUVerify: implement is-a-constant analysis	Peter Collingbourne	2012-06-15
\| \| \| \| \| \| \| \| \| \| \| \| \|	This analysis is used to generate race checking invariants for arbitrary (thread-level) constant offsets, in place of invariant generators for four specific constants (thread-id, global-id, 2D thread-id and 2D global-id) which are subsumed by the new analysis. The main motivation is to be able to recognise offsets used by word level accesses into byte arrays, which are formed from linear combinations of thread IDs and constants. This change allows us to remove the 2D and global size analyses, resulting in a 536-line net reduction in total code size.
*	Fix for structured regions.	Unknown	2012-06-14
\|
*	GPUVerify: refactor candidate invariant generators and analyses to use regions	Peter Collingbourne	2012-06-07
	The main goal of this change is to make the candidate invariant generation code and various analyses capable of handling both structured and unstructured programs. This is achieved using a high level abstraction of "regions" -- a region may either be a "root region" representing the entire implementation, or a natural loop within that implementation. Note that this is a subset to the term's meaning in the context of compilers, in which regions are also used for conditional control flow. Each region consists of a set of commands and a set of child regions. This change also has the side effect of eliminating a large amount of boilerplate code -- its net effect is to reduce the number of lines of code by 88.