debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge	qadeer	2012-04-01
\|\
* \|	commented out SuperAwesomeMethod	qadeer	2012-04-01
\| \|
\| *	bug fix for previous refactoring	Unknown	2012-04-02
\| \|
* \|	Merge	qadeer	2012-04-01
\|\\|
* \|	partial work on non-uniform loop unrolling	qadeer	2012-04-01
\| \|
\| *	Refactored CheckAssumptions API	Unknown	2012-04-02
\|/
*	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2012-03-30
\|\
\| *	Changed the BCT solution so it uses the CodePlex version of CCI (instead	Mike Barnett	2012-03-30
\| \| \| \| \| \| \| \| \| \| \| \|	of the internal version). Fixed the expression traverser to (begin the) support target expressions as operands of binary expressions. (e.g., x++ or x += 2)
* \|	Fixed bug with GPUVerify precondition generation	Unknown	2012-03-30
\| \|
\| *	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2012-03-29
\|/\|
* \|	Merge	Unknown	2012-03-28
\|\ \
* \| \|	Improved invariant inference.	Unknown	2012-03-28
\| \| \|
\| * \|	Merge	Christian Klauser	2012-03-27
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	Update test script shortcuts to work in Powershell (which supplies an ↵	Christian Klauser	2012-03-27
\| \| \| \| \| \| \| \| \| \| \| \|	absolute path as %0 instead of just the scripts name)
* \| \|	Merge	Unknown	2012-03-26
\|\ \ \
* \| \| \|	Started adding another invariant generation analysis.	Unknown	2012-03-26
\| \| \| \|
\| * \| \|	Chalice build succeeded	CodeplexBot	2012-03-26
\| \| \| \|
\| * \| \|	Switch bvd to MSIL (instead of x86) target architecture	stobies	2012-03-26
\| \| \| \|
\| * \| \|	Emit of invariants now prints out the invariant attributes also	qadeer	2012-03-26
\|/ / /
* \| \|	Merge	Unknown	2012-03-26
\|\ \ \
\| * \| \|	Chalice: Added /boogieOpt:noinfer to chalice.bat in order to run Boogie ↵	mschwerhoff	2012-03-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	without the specification inference component, because the latter is currently causing trouble with one of the AVL-tree examples.
* \| \| \|	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
\| \| \|
* \| \|	Fixed some bugs in uniformity analysis - now passes GPUVerify test suite.	Unknown	2012-03-24
\| \| \|
* \| \|	Using uniform expression analysis in GPUVerify - also did some major ↵	Unknown	2012-03-24
\| \| \| \| \| \| \| \| \| \| \| \|	refactoring to GPUVerify.
* \| \|	Merge	Unknown	2012-03-23
\|\ \ \
* \| \| \|	Added uniform expression analysis, and started using it to do less predication.	Unknown	2012-03-23
\| \| \| \|
\| * \| \|	added attributes to loop invariants	qadeer	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.
* \| \|	Merge	Unknown	2012-03-18
\|\ \ \
* \| \| \|	Support for arrays with arbitrary indices	Unknown	2012-03-18
\| \| \| \|
\| * \| \|	more type checking for datatypes	qadeer	2012-03-18
\|/ / /
* \| \|	Improved kernel precondition generation	Unknown	2012-03-17
\| \| \|
* \| \|	Merge	Unknown	2012-03-16
\|\ \ \
* \| \| \|	Added support for further annotations	Unknown	2012-03-16
\| \| \| \|
\| * \| \|	Dafny: support assign-such-that in var declarations in refinements	Unknown	2012-03-15
\| \| \| \|
\| * \| \|	Dafny: fixed lack of assign-such-that restriction in parallel statement	Unknown	2012-03-15
\| \| \| \|
\| * \| \|	Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :\| Expr;	Unknown	2012-03-15
\| \| \| \|
\| * \| \|	Dafny: added StoreAndRetrieve refinement example	Unknown	2012-03-15
\| \| \| \|
\| * \| \|	Chalice build succeeded, 73 test(s) failed	CodeplexBot	2012-03-14
\| \| \| \|
\| * \| \|	Chalice: Fix resolver bug, and add a test case for it.	stefanheule	2012-03-13
\| \| \| \|
\| * \| \|	Chalice: New test case to cover internally found bug (already fixed by ↵	stefanheule	2012-03-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	changeset 30e940802059deb4d1e600c3c1fbcda5e39128eb).
\| * \| \|	Chalice: Fix tracking of folded predicates under old().	stefanheule	2012-03-13
\| \| \| \|
\| * \| \|	Chalice: By default use the new stdin method to pass the Boogie program to ↵	stefanheule	2012-03-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Boogie. Command line options /print and /print:<file> can be used to inspect the Boogie file.
\| * \| \|	Chalice: Do not print empty conditionals.	stefanheule	2012-03-13
\| \| \| \|
\| * \| \|	Chalice: Adapt test and reference output to recent changes (previously ↵	stefanheule	2012-03-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	failing test now verifies; i.e. Chalice is less incomplete).
\| * \| \|	Chalice: Make sure secondary permissions stay positive.	stefanheule	2012-03-13
\| \| \| \|