debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Added a translation for typeof expressions.	mikebarnett	2011-03-09
\| \| \| \|	Save and restore the value of Sink.RetVariable so that it doesn't get changed during the translation of a method body when new procedures end up getting declared during the translation.
*	Can now translate multiple assemblies into one Boogie Program.	mikebarnett	2011-03-08
\| \| \| \|	Support for stub methods.
*	Fix Sink.FindOrCreateProcedure so that it takes an IMethodDefinition instead ↵	mikebarnett	2011-03-06
\| \| \| \|	of an IMethodReference so it is guaranteed to know if the method is static or not and also to be able to access its parameters as IParameterDefinitions which is needed to know if they are out params or not.
*	Added support for stub methods. If a method definition is marked with a ↵	mikebarnett	2011-03-06
\| \| \| \| \| \|	custom attribute [Stub], then no procedure declaration is created for it. The user must make sure to provide Boogie with a file containing the procedure declaration. In addition, if the attribute has a string argument, [Stub("f")], then "f" is used as the nsame of the corresponding procedure instead of the encoded name computed from the method.
*	In the Sink, keep track of any procedures defined in the initial program ↵	mikebarnett	2011-03-06
\| \| \| \|	(which is created by the heap when the initial Heap object is created). When the Sink is asked for a procedure corresponding to a method, if the method's encoded name matches any of the these procedures, then the matching procedure is returned.
*	Changes needed to translate both contracts and method bodies. The Statement ↵	mikebarnett	2011-03-05
\| \| \| \| \| \| \| \|	and Expression traversers need to have a mode that controls two things: 1. Parameters occurring in contracts are translated as the corresponding in-parameter of the corresponding procedure. Parameters occurring in method bodies are translated as the corresponding out-parameter of the corresponding procedure. 2. Method calls in method bodies are translated as call commands. Method calls in contracts are translated as function calls.
*	changes for dealing with delegates	qadeer	2011-03-05
\|
*	Fix translation of "new" so that a procedure is generated (if needed) for ↵	mikebarnett	2011-03-03
\| \| \| \|	the called ctor.
*	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.
*	Create a static constructor only for types that don't already define one.	mikebarnett	2011-03-02
\| \| \| \|	Fix a problem in two of the heaps where the AST for "type Type;" wasn't getting created.
*	put the call to CreateStaticConstructor back in	qadeer	2011-03-02
\|
*	some fixes	qadeer	2011-03-02
\| \| \| \| \|	1. introduced ProcedureInfo for packaging up relevant information about a Procedure 2. removed the call to the code that generates the static class constructor. this is temporarily broken; have to discuss with mike
*	Fix null-equivalent initialization of fields so that instance fields are ↵	mikebarnett	2011-03-02
\| \| \| \|	initialized in instance constructors and static fields are initialized in static constructors. Added wrinkle is that compiler generates a static constructor only if it needs to, so if there isn't one, we create one.
*	fixes for splitFields option	qadeer	2011-03-02
\|
*	Use the Sink's API for creating a procedure for the Invoke method of a delegate.	mikebarnett	2011-03-01
\|
*	Fixed many bugs.	mikebarnett	2011-03-01
\| \| \| \| \| \|	Ctors now initialize all fields to default (null-equivalent) values. Generate procedures for interface methods. Translate enums just by ignoring them and using the integers that they really are.
*	Fixed dynamic dispatch so the most derived override is called for each subtype.	mikebarnett	2011-02-25
\|
*	two bug fixes	qadeer	2011-02-25
\|
*	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.
*	Changed calls to Debug.Assert to Contract.Assert.	mikebarnett	2011-02-24
\| \| \| \| \|	Suppress source contexts for empty statements. Added a "whole program" option. When that is specified, then virtual calls are translated into a series of if-statements that test the dynamic type of the receiver and call the appropriate method. This is done only for subtypes that are defined in the CUA (Code Under Analysis -- which currently consists of just the one assembly being translated). [Note: currently the dynamic type is not implemented. That is next.]
*	Fix build by adding missing project.	mikebarnett	2011-02-23
\|
*	Moved the creation of Boogie procedures from the MetadataTraverser to the ↵	mikebarnett	2011-02-11
\| \| \| \|	Sink because a procedure needs to be created for every method called in the translated program and not just the methods defined in the assembly being translated. This means the contract provider is needed only in the sink and not by any of the traversers.
*	If a method definition has any custom attributes, translate them into BPL ↵	mikebarnett	2011-02-09
\| \| \| \|	attributes on the associated procedure.
*	Added support for translating delegates	qadeer	2011-02-08
\|
*	Fix the generation of procedure names so that array types are encoded properly.	mikebarnett	2011-01-26
\| \| \| \| \| \| \|	Translate "default value" expressions. Fix translation of non-trivial conditional expressions and added two more optimizations for trivial ones (trivial ones are where either the true branch or the false branch are constants). Fix translation of array length expressions. Fix translation of logical negation expressions.
*	Make the general heap representation the default.	mikebarnett	2011-01-22
\| \| \| \|	Make the pre- and post-conditions not be free contracts.
*	Added the heap representation I was supposed to have started with... A ↵	mikebarnett	2011-01-21
\| \| \| \|	general one that generates function calls for heap reads and writes so that the actual heap representation can be decided just by changing the prelude.
*	Forgot to add file with last checkin.	mikebarnett	2011-01-21
\|
*	Added a better options parsing by using functionality from MemberHelper.	mikebarnett	2011-01-21
\| \| \| \| \| \| \|	Added a new heap representation, TwoDBoxHeap. Made method names unique (previously, overloads all shared the same procedure name). As part of that, no longer require method references to be resolved in order to generate a name. Added a regression test for TwoDBoxHeap. Added tests for method overloads for unique name generation.
*	Fix order of getting the instance and the field from the expression heap so ↵	mikebarnett	2011-01-21
\| \| \| \|	that assignments are done correctly.
*	Put back the prelude for the split fields heap that had been there before.	mikebarnett	2011-01-21
\|
*	Use the interned key of field references, now that they have one.	mikebarnett	2011-01-21
\|
*	Added a test for the split fields option.	mikebarnett	2011-01-20
\| \| \| \|	Refactored some code to make it easier to work with different heap representations.
*	Renamed outside of SVN, so added the renamed file and deleting this.	mikebarnett	2011-01-20
\|
*	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.
*	Removed HeapVariable from everywhere now that it is encapsulated in the Heap ↵	mikebarnett	2011-01-19
\| \| \| \|	component.
*	Removing resolution: there's no need to resolve field references in order to ↵	mikebarnett	2011-01-18
\| \| \| \|	translate them.
*	The beginning of the encapsulation of the Heap representation so that we can ↵	mikebarnett	2011-01-17
\| \| \| \|	easily have different ways of translating the heap.
*	Fix translation of "null" so that it produces a type-correct value.	mikebarnett	2011-01-16
\|
*	1. Converted assume to assert for the source info	qadeer	2010-12-21
\| \| \| \|	2. Added tests for array translation
*	Changed attribute names in the BPL for source context assumption statements.	mikebarnett	2010-12-21
\|
*	Use an explicit PdbReader instead of the more general ↵	mikebarnett	2010-12-21
\| \| \| \|	ISourceLocationProvider so that we can get the closest source location even if the location we have doesn't correspond to an exact source location.
*	added support for array translation.	qadeer	2010-12-20
\|
*	Generate "assume {:filename "foo.cs"}{:line 3} true" statements for each ↵	mikebarnett	2010-12-20
\| \| \| \|	statement that has a source location.
*	Translate boolean types into Bpl.Type.Bool.	mikebarnett	2010-12-20
\|
*	Added Alloc implementation to the Prelude	qadeer	2010-12-15
\| \| \| \| \|	Fixed bug in translation of assume statement Added code for special handling of poirot specific calls
*	Added a new option for splitting fields	qadeer	2010-12-15
\| \| \| \|	Updated the regression input file
*	Fixed declaration of procedures from static methods so that they don't have ↵	mikebarnett	2010-12-14
\| \| \| \| \| \|	the "this" parameter. If a method definition is marked with an attribute whose name is "AsyncAttribute", then all calls to that method have {: async } added as an attribute on the call.