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
\|
*	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.
*	Add some experimental support for diagnosing timeouts.	Valentin Wüstholz	2015-05-18
\|
*	Minor change to the encoding of partially verified assertions as VC	wuestholz	2015-01-30
\|
*	Worked on the verification result caching (use native support for partially ↵	wuestholz	2015-01-16
\| \| \| \|	verified assertions).
*	Added a test and a todo.	wuestholz	2015-01-02
\|
*	Worked on more native support for partially-verified assertions.	wuestholz	2014-12-28
\|
*	Cleanup: removed unused code	akashlal	2014-09-29
\|
*	Bug fix in stratified inlining (triggered by {:inline} functions)	akashlal	2013-10-21
\|
*	fixed the problem with codexprs	qadeer	2013-09-07
\| \| \| \|	now positive/negative context is detected and appropriate translation is done
*	When a codeexpr is used at the top-level in an assume statement, we use the ↵	qadeer	2013-09-04
\| \| \| \|	alternative existential semantics.
*	More refactoring towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵	Ally Donaldson	2013-07-22
\| \| \| \|	plain Hashtable.
*	Removed old comments about "BASEMOVE" and other constructor calls, where the ↵	Unknown	2013-01-07
\| \| \| \|	conversion from Spec# into C# moved a constructor call
*	various cleanup regarding /doNotUseLabels	qadeer	2012-02-28
\|
*	bug fixes related to using ControlFlowFunction instead of labels	qadeer	2012-02-23
\|
*	using model instead of labels	Unknown	2012-02-23
\|
*	Boogie: output number of proof obligations (asserts) along with timing ↵	Rustan Leino	2012-01-09
\| \| \| \|	information when using the /trace option
*	Added lazy summary computation to stratified inlining (not finished yet)	akashlal	2011-11-20
\|
*	LetVC can get null label2absy from lazy inlining. So, I weakened the ↵	qadeer	2011-05-03
\| \| \| \|	precondition otherwise the checked build was failing
*	modified letvc generation so that the use of control flow function and ↵	qadeer	2011-04-15
\| \| \| \|	labels is decoupled. Former is controled by controlFlowVariable and the latter by label2Absy.
*	added reachability information to the VC and used that to support arbitrary ↵	Unknown	2011-04-14
\| \| \| \|	asserts in lazy inlining
*	Boogie:	rustanleino	2010-09-23
\| \| \| \| \| \|	* Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
*	Boogie: Added boolean code expressions (sans well-formedness checks on the ↵	rustanleino	2010-08-10
\| \| \| \|	input).
*	Boogie: VCGeneration port part 1/3: Replacing old source files with ported ↵	tabarbe	2010-07-28
\| \| \| \|	version
*	Boogie\VCGeneration: Renaming sources in preparation for my addition of the ↵	tabarbe	2010-07-28
	ported C# version