debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Improve support for identifying unnecessary assumes.	Valentin Wüstholz	2016-03-09
\|
*	Add support for weights on soft assumes.	Valentin Wüstholz	2016-03-07
\|
*	Improve support for optimization and identifying unnecessary assumes.	Valentin Wüstholz	2016-03-03
\|
*	Minor change	Valentin Wüstholz	2015-12-29
\|
*	Remove workaround for older versions of Z3.	Valentin Wüstholz	2015-12-02
\|
*	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.
*	Add simplified may-unverified analysis and instrumentation.	Valentin Wüstholz	2015-11-20
\|
*	Fix issue with partially-verified assertions.	Valentin Wüstholz	2015-11-19
\|
*	Add experimental support for optimization (requires Z3 build after changeset ↵	Valentin Wüstholz	2015-11-18
\| \| \| \|	9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
*	Add support for identifying unnecessary assumes.	Valentin Wüstholz	2015-11-16
\|
*	Add support for annotating implementations with k-ind. depth.	Valentin Wüstholz	2015-10-29
\|
*	Improve output for diagnosing timeouts.	Valentin Wüstholz	2015-09-30
\|
*	update	Shaz Qadeer	2015-09-28
\|
*	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.
\| *	Minor additions to VC gen	Akash Lal	2015-07-20
\| \|
\| *	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.
\| *	various changes for duality from dead codeplex repo	U-REDMOND\kenmcmil	2015-06-09
\|/
*	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-06-05
\|
*	Fix for SI: initialize extraRecBound	Akash Lal	2015-06-05
\|
*	Simplified StratifiedVC interface	akashlal	2015-06-01
\|
*	Allow for extra instrumentation on program before vc gen	Akash Lal	2015-05-25
\|
*	Add some experimental support for diagnosing timeouts.	Valentin Wüstholz	2015-05-18
\|
*	Make caching of verification results more fine-grained for changes that ↵	Valentin Wüstholz	2015-05-17
\| \| \| \|	affect preconditions.
*	Fix for printFixedPoint when dealing with functions	Akash Lal	2015-05-13
\|
*	Fix for secureVCGen	Akash Lal	2015-05-07
\|
*	Make it preserve the fact that the value of an assumption variable never ↵	Valentin Wüstholz	2015-05-06
\| \| \| \|	becomes logically weaker after a havoc.
*	VC gen for security properties	akashlal	2015-04-05
\|
*	Compute MustReach information lazily, on-demand	akashlal	2015-03-16
\|
*	Added MustReach information to VC gen	akashlal	2015-03-11
\|
*	Made it produce slightly different passive commands for assignments to ↵	wuestholz	2015-01-30
\| \| \| \|	assumption variables.
*	Minor change to the encoding of partially verified assertions as VC	wuestholz	2015-01-30
\|
*	Handle timeout in refinement loop	akashlal	2015-01-28
\|
*	Fixed minor issue.	wuestholz	2015-01-26
\|
*	Minor change	wuestholz	2015-01-26
\|
*	Worked on the verification result caching (trace output).	wuestholz	2015-01-26
\|
*	Worked on the verification result caching (use native support for partially ↵	wuestholz	2015-01-16
\| \| \| \|	verified assertions).
*	Fix related to limitations in CVC4 model parsing	Ally Donaldson	2015-01-14
\|
*	Added a test and a todo.	wuestholz	2015-01-02
\|
*	Worked on more native support for partially-verified assertions.	wuestholz	2014-12-28
\|
*	Fixed a postcondition.	wuestholz	2014-12-26
\|
*	Added an annotation, :split_here, for predicate statements.	Bryan Parno	2014-12-16
\| \| \| \| \| \|	The annotation allows the programmer to manually indicate where the verification of a procedure implementation should be split into pieces.
*	Merge some FixpointVC changes that got left behind	Ken McMillan	2014-12-08
\|\
* \|	Optimized the VC generation for assumption variables.	wuestholz	2014-12-07
\| \|
* \|	Fixed issue in the verification result caching.	wuestholz	2014-11-10
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-10
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-05
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-03
\| \|
* \|	Worked on the verification result caching.	wuestholz	2014-11-03
\| \|
* \|	Fixed minor issue.	wuestholz	2014-11-02
\| \|