debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	When translating an assighment, leave the source of the assignment on the	Unknown	2012-06-02
\| \| \| \|	stack in case it is needed by an enclosing expression.
*	Don't add dummy modules (resulting from a failed load) to the list of modules	Unknown	2012-06-02
\| \| \| \|	to be translated.
*	Fix for addressof expressions.	Unknown	2012-05-18
\|
*	Add options to control the emission of free ensures for	Unknown	2012-04-16
\| \| \| \| \| \|	heap monotonicity (and allocatedness of references returned from a method) as well as the assert/assume checks that are generated for every object dereference.
*	Removed expression simplifier (actually just commented	Unknown	2012-04-15
\| \| \| \| \| \| \|	it out for now) and used a simpler scheme for always assigning compound bound expressions to a local. Added the ability to assert/assume that an object is non-null before dereferencing it.
*	Added "free ensures" to procedures encoding the allocatedness	Unknown	2012-04-10
\| \| \| \|	of references.
*	Fix a lot of the translation of "op=" expressions	Unknown	2012-04-09
\| \| \| \|	(like += or *=).
*	Changed the BCT solution so it uses the CodePlex version of CCI (instead	Mike Barnett	2012-03-30
\| \| \| \| \| \|	of the internal version). Fixed the expression traverser to (begin the) support target expressions as operands of binary expressions. (e.g., x++ or x += 2)
*	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2012-03-29
\|\
* \|	updated Boogie strings so that they can refer to \" (and more)	qadeer	2012-03-12
\| \| \| \| \| \| \| \|	fixed BCT :value
\| *	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2012-03-11
\|/\|
\| *	more work on op-assign expressions. (unfinished)	Mike Barnett	2012-03-11
\| \|
* \|	further sanitization of string in :value attribute	qadeer	2012-03-11
\| \|
* \|	added breadcrumb to the beginning of each method	qadeer	2012-03-09
\| \|
* \|	value attribute "\n" to "\\n"	qadeer	2012-03-01
\| \| \| \| \| \| \| \|	more work is perhaps needed to handle all cases
\| *	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2012-02-27
\|/\|
\| *	Adapting to new decompiler.	Mike Barnett	2012-02-27
\| \| \| \| \| \| \| \|	Dynamic dispatch for interface method calls.
* \|	adding attribute for string literals	qadeer	2012-02-27
\| \|
* \|	added :first attribute to the first line directive corresponding to a source ↵	qadeer	2012-02-13
\|/ \| \| \|	line
*	Union is now based on axioms	qadeer	2012-02-07
\| \| \| \|	added more inline attributes
*	fixed bug in model parsing	qadeer	2012-02-06
\| \| \| \|	converted a bunch of definitions to be inlined
*	Merge	qadeer	2012-02-06
\|\
* \|	added inlining support for all implementations given the attribute {:inline 1}	qadeer	2012-02-06
\| \| \| \| \| \| \| \| \| \|	removed AssertionInjector from the solution changed the representation of multicast delegates
\| *	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2012-02-05
\|/\|
\| *	Separated the concepts of "boxing" (i.e., CLR boxing of a value type) from	Mike Barnett	2012-02-05
\| \| \| \| \| \| \| \|	the "union" type that is the supertype of all the translated Boogie types.
* \|	added a dummy sourceLine attribute for delegate dispatch	qadeer	2012-01-31
\| \|
* \|	added another project	qadeer	2012-01-30
\| \|
\| *	Automated merge with https://hg01.codeplex.com/boogie	Mike Barnett	2012-01-26
\| \|\
\| \| *	Separate out the concepts of boxing	Mike Barnett	2012-01-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(i.e., CLR's creating a heap cell and putting a value into it) from the concept of the "union" type that all Boogie types are a subtype of.
* \| \|	added another method that just throws an exception	qadeer	2012-01-24
\|/ /
* /	an optimization in dynamic dispatch	qadeer	2012-01-23
\|/ \| \| \|	a hack in event translation
*	Mark the procedure translated from the module's entry point	Mike Barnett	2012-01-15
\| \| \| \|	with the attribute {:entrypoint}.
*	Make a copy of a struct value being passed to a method	Mike Barnett	2012-01-10
\| \| \| \|	whether the method is generic or not.
*	Fix call to struct copy ctor.	Mike Barnett	2012-01-10
\|
*	Fixed struct copy constructor implementation.	Mike Barnett	2012-01-10
\|
*	Change the copy constructor for struct types so that it returns the copy	Mike Barnett	2012-01-09
\| \| \| \| \|	of the struct value. This way it can do an allocation within the copy ctor (if that is the design choice for structs, which it currently is).
*	Copy structs that are passed by value as method call arguments.	Mike Barnett	2012-01-04
\| \| \| \|	Define body for default struct ctors.
*	For now, just ignore "address of" nodes and translate the expression of which	Mike Barnett	2012-01-03
\| \| \| \|	the address is being taken.
*	new axioms for subtyping	qadeer	2011-12-31
\|
*	modeling multiset using generalized array theory	qadeer	2011-12-30
\|
*	made delegate a datatype	qadeer	2011-12-30
\| \| \| \|	added a DatatypeConstructor class
*	problem fixed after CCI update	qadeer	2011-12-30
\|
*	fixed problems with datatypes	qadeer	2011-12-29
\| \| \| \| \|	removed stale contracts in stratified inlining added test to datatypes
*	Merge	qadeer	2011-12-28
\|\
* \|	deleted some commented code	qadeer	2011-12-28
\| \|
\| *	Add instrumentation for branches.	Mike Barnett	2011-12-28
\|/
*	refactored AssertionInjector so that it works directly on bpl files as well	qadeer	2011-12-26
\|
*	bug fix in houdini inlineDepth	qadeer	2011-12-06
\|
*	Fixed bug when getting last source context in a method body.	Mike Barnett	2011-12-06
\|
*	Refactored translator so it can be called programmatically and return the	Mike Barnett	2011-11-21
\| \| \| \|	translated program in memory without writing it to disk.