debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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
\|
*	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.
*	Minor refactoring	Valentin Wüstholz	2015-05-17
\|
*	Make caching of verification results more fine-grained for changes that ↵	Valentin Wüstholz	2015-05-17
\| \| \| \|	affect preconditions.
*	Add support for 'verified_under' attributes on procedure calls and invariants.	Valentin Wüstholz	2015-04-29
\|
*	Worked on the verification result caching (statement checksums).	wuestholz	2015-01-26
\|
*	Merging changes from wuestholz/BoogieInvariantFixesIIII	wuestholz	2015-01-13
\|\
\| *	Made invariant of class 'StmtList' robust by:	wuestholz	2015-01-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- making field private and readonly - exposing IEnumerable - adding 'AddLabel' method (with help from David Rohr)
\| *	Made invariant of class 'StmtList' robust by:	wuestholz	2015-01-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- adding private field - exposing read-only list - copying incoming list (with help from David Rohr)
\| *	Made invariant of class 'QKeyValue' robust by:	wuestholz	2015-01-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- making field private - exposing read-only list - copying incoming list - adding methods 'AddParam', 'AddParams', and 'ClearParams' (with help from David Rohr)
\| *	Made invariant of class 'EEDTemplate' robust by:	wuestholz	2015-01-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- making field private - exposing an IEnumerable - copying incoming list (with help from David Rohr)
\| *	Made invariant of class 'Block' robust by:	wuestholz	2015-01-09
\| \| \| \| \| \| \| \| \| \| \| \|	- making field private - exposing an IEnumerable (with help from David Rohr)
* \|	Made invariant of class 'ListOfMiningStrategies' robust by changing the design	0biha	2015-01-01
\| \| \| \| \| \| \| \|	(replaced public field by private field + getter/setter)
* \|	Made 2 invariants of class 'IfCmd' robust by changing the design	0biha	2015-01-01
\| \| \| \| \| \| \| \|	(replaced public fields by private fields + getters/setters)
* \|	Made invariant of class 'EEDTemplate' robust by changing the design	0biha	2015-01-01
\| \| \| \| \| \| \| \|	(replaced public field by private field + getter/setter)
* \|	Made invariant of class 'StructuredCmd' robust by changing the design	0biha	2015-01-01
\| \| \| \| \| \| \| \|	(replaced public field by private field + getter/setter)
* \|	Made 2 invariants of class 'Block' robust by changing the design	0biha	2015-01-08
\| \| \| \| \| \| \| \|	(replaced public fields by private fields + getters/setters)
* \|	Made 3 invariants of class 'BigBlock' robust by changing the design	0biha	2015-01-01
\| \| \| \| \| \| \| \|	(replaced public fields by private fields + getters/setters)
* \|	Made invariants of classes 'Requires' and 'Ensures' robust by making ↵	0biha	2014-12-27
\|/ \| \| \|	'IPotentialErrorNode' generic.
*	Minor changes	wuestholz	2015-01-02
\|
*	Worked on more native support for partially-verified assertions.	wuestholz	2014-12-28
\|
*	Minor precondition fix	0biha	2014-12-26
\|
*	Replaced properties Lhss_NRO and Rhss_NRO by methods SetLhs and SetRhs.	0biha	2014-12-25
\|
*	Made some compatibility fixes after running the unit tests.	0biha	2014-12-24
\| \| \| \|	Added an internal non-readonly version of Lhss and Rhss to 'AssignCmd'.
*	Made invariant of class 'HavocCmd' robust by changing the design (replaced ↵	0biha	2014-12-19
\| \| \| \|	public field by private field + getter/setter).
*	Made 2 invariants of type 'StateCmd' robust by changing the design	0biha	2014-12-19
\| \| \| \|	(replaced public fields by private fields + getters/setters).
*	Made 2 invariants of type 'AssignCmd' robust by	0biha	2014-12-19
\| \| \| \| \| \|	-replacing public fields by private fields + getters/setters, -making setters and constructor create a copy of the arguments, -making getters return read-only lists.
*	Reverted a change to CreateTempVariable for FixedPointVC only.	Ken McMillan	2014-12-08
\|
*	Added todos.	wuestholz	2014-11-26
\|
*	Worked on the verification result caching (extracted functions).	wuestholz	2014-11-25
\|
*	Fixed issues in the verification result caching (old expressions).	wuestholz	2014-11-24
\|
*	Fixed issue in the verification result caching.	wuestholz	2014-11-10
\|
*	Worked on the verification result caching.	wuestholz	2014-11-10
\|
*	Made it never include the statement checksum when printing assert statements.	wuestholz	2014-11-16
\|
*	Minor refactoring	wuestholz	2014-11-05
\|
*	Worked on the verification result caching.	wuestholz	2014-11-05
\|
*	Made it produce more trace output for the verification result caching.	wuestholz	2014-11-02
\|
*	Fixed an issue (reported by Akash Lal).	wuestholz	2014-10-30
\|
*	Worked on the verification result caching.	wuestholz	2014-10-19
\|
*	Worked on the verification result caching.	wuestholz	2014-10-19
\|
*	Worked on the verification result caching.	wuestholz	2014-10-17
\|
*	Worked on the verification result caching.	wuestholz	2014-10-17
\|
*	Worked on the verification result caching.	wuestholz	2014-10-17
\|
*	Worked on the verification result caching.	wuestholz	2014-10-17
\|
*	Minor change	wuestholz	2014-10-16
\|
*	Worked on the verification result caching.	wuestholz	2014-10-15
\|
*	Fix issue in computation of checksums for calls.	wuestholz	2014-10-15
\|
*	Fix issue in computation of checksums for assume statements.	wuestholz	2014-10-14
\|
*	Implement ToString() override for TransferCmds. It is overriden for	Dan Liew	2014-10-13
\| \| \| \| \|	Cmd classes but for some reason it wasn't implemented for TransferCmds which seems a little inconsistent.