debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Many, many bug fixes related to generics and some other random problems.	Mike Barnett	2011-11-10
\|
*	Major changes to the translator traversers because they now are based on the	Mike Barnett	2011-10-31
\| \| \| \| \| \| \| \|	new traversers. (The old ones have been marked as obsolete.) All types are now encoded as "datatypes" in Boogie. So non-generic types are nullary functions and generic types just have at least one type argument. Lots of other fixes: string encoding of names is now done by negating Boogie's regular expression for identifiers, etc.
*	delegates/events implemented as multisets rather than linked lists	qadeer	2011-08-30
\|
*	added RealModulus	qadeer	2011-08-17
\|
*	fixes for bug with generic delegates	qadeer	2011-08-11
\|
*	(phone bct) nav graph building (mostly) automated	t-espave	2011-08-05
\|
*	Increase the name mangling to avoid name clashes in the Boogie program. In IL,	Mike Barnett	2011-08-03
\| \| \| \|	members of a type can have the same name.
*	(phone bct) default URI checks inlined	t-espave	2011-08-02
\| \| \| \|	inlining statistics
*	fixed right/left shift functions decl	t-espave	2011-07-27
\|
*	added translation for RightShift and LeftShift	Unknown	2011-07-26
\|
*	double definition fix	t-espave	2011-07-22
\| \| \| \|	changed functions to maps for control properties
*	Added subtyping axiomatization.	Mike Barnett	2011-07-20
\|
*	edited out phoneplugin from most places	Unknown	2011-07-19
\| \| \| \| \|	havoc'ing uri when navigation cannot be determined (partial) added boilerplate boogie code
*	potentially useful boogie stubs, commented out since they may conflict with ↵	Unknown	2011-07-15
\| \| \| \|	{:extern}
*	Beginning of encoding the subtype relation.	Mike Barnett	2011-07-06
\|
*	bug fix in heap access for splitfield option	qadeer	2011-06-30
\|
*	whole bunch of bug fixes	qadeer	2011-06-20
\|
*	Real2Int type error	Unknown	2011-06-15
\|
*	refactored the prelude, added thread_local attribute to $Exception variable	qadeer	2011-06-14
\|
*	various bug fixes related to running bct on phone apps	qadeer	2011-06-12
\|
*	changes related to fixing problems with finally translation	qadeer	2011-06-12
\|
*	Further support for translating generics	qadeer	2011-06-04
\|
*	Added bitwise operations.	Mike Barnett	2011-05-31
\|
*	Lots of small bug fixes: conversions, overloaded operations on real numbers.	Mike Barnett	2011-05-31
\|
*	Handle more conversions.	Mike Barnett	2011-05-29
\|
*	Fixes for a bunch of different bugs. Translate default value for doubles,	Mike Barnett	2011-05-29
\| \| \| \| \|	handle structs that call the default ctor on "this", translate conversion from object to double, etc.
*	Beginning of representing structs as values on the heap, but without object	Mike Barnett	2011-05-26
\| \| \| \| \|	equality. Now each struct type has a default constructor that sets all of its fields to zero-equivalent values.
*	Fixed array construction	qadeer	2011-05-17
\| \| \| \|	Added a couple more stubs
*	first cut at handling generics	qadeer	2011-05-11
\|
*	More support for reals, especially real constants.	Mike Barnett	2011-05-08
\|
*	Better error handling.	Mike Barnett	2011-05-08
\| \| \| \| \|	Defined a new Boogie type, Real, that will be used to represent floating point numbers.
*	Fixed lots of bugs having to do with casts, conversions, and address-of	Mike Barnett	2011-05-03
\| \| \| \| \| \|	expressions. Changed lots of the Boogie methods to take the "right" types, e.g., Ref instead of int.
*	Merge	Mike Barnett	2011-05-03
\|\
\| *	Trying to fix "boxing", i.e., value type to ref conversions as done in the CLR.	Mike Barnett	2011-05-03
\| \|
* \|	bug fixes related to handling of structs, arrays, and assignments	qadeer	2011-05-02
\|/
*	Model newly constructed structs as a constant DefaultStruct that has axioms that	Unknown	2011-04-27
\| \| \| \|	define it to return zero-equivalent values for all fields.
*	fixing problems with struct translation	qadeer	2011-04-27
\|
*	0. Deleted other heap representations except SplitField and General	qadeer	2011-04-23
\| \| \| \|	1. first cut at implementing structs
*	Fix stub support (still not completely finished).	Unknown	2011-04-12
\| \| \| \| \| \|	Fix generation of delegate methods so that they happen after translating all input assemblies and not per assembly. Fix translation of typeof() expressions.
*	Made it unnecessary to set the types on the Boogie ASTs as we create them.	mikebarnett	2011-03-03
\| \| \| \| \| \|	Added support for string literals. Translating structs no longer crashes the translator, but on the other hand, they are just skipped and not translated... Added a helper method to make sure that generated identifiers are Boogie-legal.
*	fixes for splitFields option	qadeer	2011-03-02
\|
*	implemented delegates and events	qadeer	2011-02-25
\|
*	Added a new type, Type, that represents runtime types. The Heap interface ↵	mikebarnett	2011-02-24
\| \| \| \| \| \|	now provides a way to declare a new user-defined type and to represent the expressions "typeof(T)" or "o.Type" in the BPL program using a new function $DynamicType. Added a method to the Sink so that any of the translation visitors can find or declare a new type. When an object is allocated, an assumption is generated that gives its dynamic type. Fixed the dynamic dispatch inlining so that the $DynamicType of the object is used to decide which override to call.
*	Moved the parts of the Prelude that depend on the heap representation into ↵	mikebarnett	2011-01-20
\| \| \| \| \| \|	the appropriate Heap objects. Also added the ability to easily have access to the ASTs that result from the specific heap representation's declarations.
*	More structuring of the different heap representations. Now each heap ↵	mikebarnett	2011-01-19
	representation is implemented as a different object.