debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merging complete. Everything looks good crosses fingers	Checkmate50	2016-06-06
\|
*	Let attributes live on during inlining	akashlal	2014-11-05
\|
*	Did more refactoring and addressed several todos.	wuestholz	2014-09-23
\|
*	Did some refactoring.	wuestholz	2014-09-23
\|
*	a small fix to prefix calculation	qadeer	2014-09-19
\|
*	a bug fix in Houdini (also AbsHoudini)	qadeer	2014-09-19
\|
*	InlineAssume attribute for ensures clauses; if present, the ensures ↵	qadeer	2014-09-18
\| \| \| \|	condition is assumed while inlining.
*	added a comment	qadeer	2014-09-17
\|
*	fixed a bug in inlining	qadeer	2014-09-17
\| \| \| \|	changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"
*	Fix nasty bug introduced by commit 61a94f409975.	Dan Liew	2014-07-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
*	fixed code contracts violations	qadeer	2014-02-11
\|
*	Remove some (redundant) preconditions to avoid 'ccrewrite' errors.	wuestholz	2013-12-11
\|
*	minor fix so that variable copies in procedures and codeexprs are different.	qadeer	2013-09-10
\|
*	inlining is now done in rhs of assignments for codeexprs	qadeer	2013-08-15
\| \| \| \|	added more regressions
*	Extended codeexpr inlining to deal with nested codeexpr	qadeer	2013-08-15
\| \| \| \|	Added a regression
*	extended inlining to deal with codeexprs	qadeer	2013-08-14
\|
*	StringSeq: farewell	Ally Donaldson	2013-07-22
\|
*	CmdSeq: farewell	Ally Donaldson	2013-07-22
\|
*	Started to remove ...Seq classes	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring: PureCollections.Sequence not used anymore.	Ally Donaldson	2013-07-22
\|
*	More refactoring towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	Changed Has method of PureSequence to Contains to make refactoring easier.	Ally Donaldson	2013-07-22
\|
*	Requires/EnsuresSeq replaced by List<Requires/Ensures>	Ally Donaldson	2013-07-22
\|
*	Large refactoring of Hashtable to Dictionary.	Ally Donaldson	2013-07-22
\|
*	Added a little bit of virtual-ness to the Inliner class. This is so that I can	akashlal	2013-04-28
\| \| \| \|	subclass it to implement my own inlining policy.
*	bug fix for interaction between inlining and loops	Unknown	2013-01-04
\|
*	changed behavior of InlinedEnsures so that free ensures is skipped unless an ↵	qadeer	2012-06-01
\| \| \| \|	attribute called :assume is there
*	fixed a completeness problem in houdini with inlining	qadeer	2011-12-18
\|
*	fixed bug in the inlineDepth option for houdini	qadeer	2011-11-23
\| \| \| \|	small clean up in the inlining implementation
*	changed the semantics of requires and ensures for inlined procedures	qadeer	2011-11-17
\|
*	changed inlining code so that candidate preconditions and postconditions are ↵	qadeer	2011-11-15
\| \| \| \|	ignored
*	added the option /inlineDepth:n. This option defaults to -1. If the user ↵	qadeer	2011-11-13
\| \| \| \| \| \|	provides a non-negative number then that number is used to inline procedures not annotated by {:inline n} attribute.
*	Boogie: Get rid of {:inline} attributes on axioms	Michal Moskal	2011-10-27
\|
*	Replaced all dictionaries that mapped to bool (i.e., were being used to ↵	mikebarnett	2011-03-10
\| \| \| \|	implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
*	Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵	mikebarnett	2011-03-10
\| \| \| \| \| \|	dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
*	fixed a small bug in inline code	qadeer	2010-12-20
\|
*	Cleanup up the inlining code	qadeer	2010-12-15
\| \| \| \| \|	1. For some reason, constructors weren't being inlined. Now they can be. 2. Cleaned up the search for implementations
*	Boogie: Committing changed source files	tabarbe	2010-08-20
\|
*	Boogie: Renaming core sources in preparation for port commit	tabarbe	2010-08-20