debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Improve support for optimization and identifying unnecessary assumes.	Valentin Wüstholz	2016-03-03
\|
*	Merge pull request #30 from qunyanm/type-parameter-bug-fix	RustanLeino	2016-02-12
\|\ \| \| \| \|	Bug fix in determining whether a type parameter is bounded
* \|	added an example	Shaz Qadeer	2016-02-09
\| \|
* \|	another fix	Shaz Qadeer	2016-01-26
\| \|
* \|	improved some of the annotations	Shaz Qadeer	2016-01-21
\| \|
* \|	some fixes	Shaz Qadeer	2016-01-19
\| \|
\| *	Bug fix in determining whether a type parameter is bounded	qunyanm	2016-01-19
\|/ \| \| \| \| \|	When checking whether a type parameter could be determined from the bound variable types, we mistakenly compare equality between a TypeVarable and a VCExprVar, instead of between two VCExprVars.
*	updated the example to implement the allocation of thread identifiers;	Shaz Qadeer	2016-01-17
\| \| \| \| \|	this example provides another illustration of abstracting ordinary variables by linear variables
*	fixed a small problem in the precondition for FreeLinear	Shaz Qadeer	2016-01-10
\|
*	added Free code	Shaz Qadeer	2016-01-08
\|
*	Improve precision of abstract interpreter for modulo operations.	Valentin Wüstholz	2015-12-28
\|
*	Use the EndCurly token when creating the ReturnCmd for unifiedExit	qunyanm	2015-12-02
\| \| \| \| \| \| \| \|	When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block.
*	Update test output for Z3 4.4.1.	Valentin Wüstholz	2015-12-01
\|
*	Fix issue with partially-verified assertions.	Valentin Wüstholz	2015-11-19
\|
*	Update test output after Nikolaj's enhancement in Z3.	Valentin Wüstholz	2015-11-19
\|
*	Add a test.	Valentin Wüstholz	2015-11-19
\|
*	Minor changes	Valentin Wüstholz	2015-11-19
\|
*	Improve experimental support for optimization (requires Z3 changeset ↵	Valentin Wüstholz	2015-11-18
\| \| \| \|	5948013b1b04d8529bce366c0c7b87e1d88a1827 or later).
*	Add experimental support for optimization (requires Z3 build after changeset ↵	Valentin Wüstholz	2015-11-18
\| \| \| \|	9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
*	Fix test output.	Valentin Wüstholz	2015-11-17
\|
*	Fix issue #25.	Valentin Wüstholz	2015-11-17
\|
*	Add a test.	Valentin Wüstholz	2015-11-16
\|
*	Add a test.	Valentin Wüstholz	2015-11-16
\|
*	Add support for identifying unnecessary assumes.	Valentin Wüstholz	2015-11-16
\|
*	Added test cases for the new asterisk wildcard behaviour of the	Dan Liew	2015-10-31
\| \| \| \|	``-proc`` command line argument.
*	fix for deterministicExtractLoops for nested loops	Shuvendu Lahiri	2015-10-27
\|
*	fixed	Shaz Qadeer	2015-10-26
\|
*	Bug fix for deterministExtractLoops for Shaobo's example	Shuvendu Lahiri	2015-10-26
\|
*	bug fix in the type checking of calls to atomic procedures	Shaz Qadeer	2015-10-16
\|
*	bug fix	Shaz Qadeer	2015-10-09
\|
*	another fix requested by Chris	Shaz Qadeer	2015-10-01
\| \| \| \|	verification is performed now for all created layers
*	fixed a small bug	Shaz Qadeer	2015-09-27
\|
*	added introduced and ghost local variables	Shaz Qadeer	2015-09-25
\|
*	fixed a crash when there is no collector	Shaz Qadeer	2015-09-02
\|
*	Merge branch 'master' of https://github.com/boogie-org/boogie	Rustan Leino	2015-08-28
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: Source/Core/CommandLineOptions.cs Source/ExecutionEngine/ExecutionEngine.cs Source/ExecutionEngine/VerificationResultCache.cs Source/VCGeneration/VC.cs Test/snapshots/runtest.snapshot Test/snapshots/runtest.snapshot.expect
* \|	Added /verifySnapshots:3, which prints recycled errors messages with the ↵	Rustan Leino	2015-08-28
\| \| \| \| \| \| \| \|	source locations of the new code.
\| *	Added another test.	Valentin Wüstholz	2015-07-20
\| \|
\| *	Added more tests.	Valentin Wüstholz	2015-07-20
\| \|
\| *	Try to unbreak the tests added in	Dan Liew	2015-06-28
\| \| \| \| \| \| \| \|	7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf under Windows.
\| *	Fix issue #16 reported by @crazykt	Dan Liew	2015-06-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously when Boogie was passed the ``-proc:<NAME>`` argument on the command line it would verify any procedure whose name contained ``<NAME>`` which doesn't seem like correct behaviour. Now Boogie only tries to verify a procedure only if its name matches ``<NAME>`` exactly. I've added several test cases to check Boogie behaves as expected.
\| *	Normalise line endings using a .gitattributes file. Unfortunately	Dan Liew	2015-06-28
\| \| \| \| \| \| \| \| \| \| \| \|	this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
\| *	updated with Serdar's changes	qadeer	2015-06-25
\| \|
\| *	added another sample	qadeer	2015-06-17
\| \|
\| *	modified desugaring so that in commutatitivity checks copies of original	qadeer	2015-06-17
\| \| \| \| \| \| \| \|	codeexpr is made.
\| *	fixed bug reported by Chris	qadeer	2015-06-15
\| \|
\| *	Fix issue with computation of statement checksums for lambda expressions.	Valentin Wüstholz	2015-06-12
\| \|
\| *	Add a test case.	Valentin Wüstholz	2015-06-12
\| \|
\| *	relaxed the check for created and hidden layers for skip actions	qadeer	2015-06-10
\| \|
\| *	fixed crash	qadeer	2015-06-10
\|/
*	bug fix in pop	qadeer	2015-05-27
\|