debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge	Mike Barnett	2011-07-01
\|\
\| *	bug fix in heap access for splitfield option	qadeer	2011-06-30
\| \|
* \|	Merge	Mike Barnett	2011-06-29
\|\\|
\| *	bug fix in translation of dispatch continuation	qadeer	2011-06-23
\| \|
\| *	Translate IConditional exactly the same way as IConditionalStatement to ↵	qadeer	2011-06-20
\| \| \| \| \| \| \| \|	account for side-effects in expressions
\| *	whole bunch of bug fixes	qadeer	2011-06-20
\| \|
\| *	Merge	qadeer	2011-06-17
\| \|\
\| * \|	changes for handling conversions	qadeer	2011-06-17
\| \| \|
\| \| *	removed division hadling from CLRsemantics	Unknown	2011-06-16
\| \|/ \| \| \| \| \| \|	fixed unarynegation issue
\| *	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
\| \|
\| *	further changes	qadeer	2011-06-12
\| \|
\| *	changes related to fixing problems with finally translation	qadeer	2011-06-12
\| \|
\| *	Merge	qadeer	2011-06-10
\| \|\
\| * \|	bunch of changes related to finally handling	qadeer	2011-06-10
\| \| \|
\| \| *	solved	Unknown	2011-06-09
\| \|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	-- conflict between int and short -- method calls type definitions -- exception returning outvar count (?) -- nested addressing issue in parameters -- enum arguments as literals -- initially declared boogie procedures are public now
\| *	using registerAsLatest directly to deal with multiple dll translation	Unknown	2011-06-08
\| \|\
\| * \|	bug fixes	Unknown	2011-06-08
\| \| \|
\| \| *	bug fix in call to constructor of ProcedureInfo	qadeer	2011-06-08
\| \| \|
\| \| *	beginning support for finally clauses	qadeer	2011-06-07
\| \| \|
\| \| *	initial cut for translating exceptions	qadeer	2011-06-06
\| \|/
\| *	fixed calls to generic methods to add type argument appropriately	qadeer	2011-06-05
\| \|
\| *	Further support for translating generics	qadeer	2011-06-04
\| \|
* \|	Don't (for now) consider property getters as pure, because	Mike Barnett	2011-06-01
\| \| \| \| \| \| \| \|	we aren't ready to translate them as functions yet.
\| *	fixed a bug in translation of generics	qadeer	2011-05-31
\| \|
\| *	Merge	qadeer	2011-05-31
\| \|\ \| \|/ \|/\|
\| *	fixed a bug with array index translation	qadeer	2011-05-31
\| \|
* \|	Fixed/improved the handling of conditional expressions.	Mike Barnett	2011-05-31
\| \|
* \|	Added bitwise operations.	Mike Barnett	2011-05-31
\| \|
* \|	Lots of small bug fixes: conversions, overloaded operations on real numbers.	Mike Barnett	2011-05-31
\| \|
* \|	Don't translate method contracts until method information (parameter map, etc.)	Mike Barnett	2011-05-30
\|/ \| \| \| \| \| \| \|	have been created since they are needed during the translation of the contracts. Don't let errors that occur during the translation of a method's custom attributes stop the translation of the method body. Added an override for translating IExclusiveOr nodes, but the translation is currently incorrect. (It just translates it as a logical or.)
*	Handle more conversions.	Mike Barnett	2011-05-29
\|
*	Fixed struct ctors so that they don't return the "this" value, but just	Mike Barnett	2011-05-29
\| \| \| \| \| \| \|	operate on the "this" parameter since it is now a Ref. Fixed the construction of the sink's "this" parameter so that it gets created anew for each method, since it will become a local variable of the method, if the method is a struct ctor.
*	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.
*	Removed the method DefaultValue from the sink: if a default value of a type	Mike Barnett	2011-05-29
\| \| \| \| \|	is desired, then the CCI nodes must be created and an expression/statement traverser used to translate it.
*	When translating the "thisArgument" of a method call, if it translates to an	Mike Barnett	2011-05-29
\| \| \| \| \| \|	expression and not just an identifier, as for instance it does for "this.f.M(...)", then generate a new local to hold the value of the "thisArgument" and return the new local as the "thisExpr".
*	Fix translation for field dereference when the type of the field is a struct.	Mike Barnett	2011-05-28
\|
*	Translate assignments to parameters that are of a struct type correctly. Note	Mike Barnett	2011-05-28
\| \| \| \| \| \|	that this means all methods with such parameters (where the parameter is passed by value) must have free preconditions expressing that the parameters are disjoint (since we are representing structs as Ref).
*	Translate assignments of structs as a call to a (default) copy constructor	Mike Barnett	2011-05-27
\| \| \| \|	that does the field-by-field copy.
*	Merge	Mike Barnett	2011-05-26
\|\
* \|	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.
\| *	merge	Sam Blackshear	2011-05-24
\| \|\ \| \|/ \|/\|
\| *	New example to demonstrate exception support that would be convenient for ↵	Sam Blackshear	2011-05-24
\| \| \| \| \| \| \| \|	Boogie.
* \|	Created an API so that a MetadataTraverser is used to translate a set of	Mike Barnett	2011-05-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	assemblies. This enables a translator to do whole-program analyses, such as recording the subtype relationship across all of the input. (Still need to move the delegate translation into this method.) Fixed the existing whole-program translator so it uses the base class functionality for translating the arguments to a method call. Updated the regressions.
* \|	Merge	Mike Barnett	2011-05-19
\|\ \
* \| \|	Unify translation of arguments so the same code is used for IMethodCall and	Mike Barnett	2011-05-19
\| \| \| \| \| \| \| \| \| \| \| \|	ICreateObjectInstance.
\| * \|	fixed the axiom about TypeOf	Unknown	2011-05-18
\|/ /
* \|	Fixed array construction	qadeer	2011-05-17
\| \| \| \| \| \| \| \|	Added a couple more stubs
* \|	added another axiom	Unknown	2011-05-17
\| \|