debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	(phone bct) compute fixpoint for necessary inlined methods (for modular ↵	t-espave	2011-08-01
\| \| \| \|	analysis)
*	adding checks and code injection for phone feedback checking	t-espave	2011-07-25
\|
*	- keeping track of BCT name changes to controls	Unknown	2011-07-15
\| \| \| \|	- injecting navigation changes code
*	- navigation event detection	Unknown	2011-07-14
\| \| \| \|	- (some) URI declaration/instantiation and use detection
*	phone injecting code traverser	Unknown	2011-07-08
\|
*	phone control exploration for BCT, not integrated yet	Unknown	2011-07-07
\| \| \| \|	should be made into a plugin sometime
*	Merge	Mike Barnett	2011-05-16
\|
*	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.]
*	More structuring of the different heap representations. Now each heap ↵	mikebarnett	2011-01-19
\| \| \| \|	representation is implemented as a different object.
*	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.
*	Add a reference to ParserHelper.dll for the definition of IToken which was ↵	mikebarnett	2010-12-09
\| \| \| \|	moved into that assembly.
*	Adapt to new APIs in CCI.	mikebarnett	2010-12-08
\|
*	Introduction of the Sink: a global object that is threaded through all of ↵	mikebarnett	2010-07-02
\| \| \| \|	the traversers and which contains the information that they need to share with each other.
*	Simplified the translator by merging the ToplevelTraverser, ClassTraverser, ↵	mikebarnett	2010-06-28
\| \| \| \|	and MethodTraverser into one traverser: MetadataTraverser. It will have to do a little more work to keep its state consistent (like saving any type-related state before traversing a nested type definition), but it seems worth it.
*	Added the factory pattern so that all traversers are created through factory ↵	mikebarnett	2010-06-16
\| \| \| \| \| \| \|	methods. This is the beginning of allowing plugins to perform methodology-specific translations. Added a CLR traverser that is meant to encode the CLR semantics. For now it just does one thing: add the assertion that a divisor should not be zero. Added an MS Test project so that we can use that for regression testing.
*	Updated the project to .NET v4.0.	mikebarnett	2010-06-06
\| \| \| \| \| \| \| \|	Added helper methods to the statement traverser. Handle ILocalDeclarationStatement, IAssertStatement, IAssumeStatement in StatementTraverser. Handle simple logical-and and logical-or expressions in ExpressionTraverser. Inject assertion that divisor is non-zero for IDivision in ExpressionTraverser. Added static variable BCT.Host so all parts of translation can access the CCI Metadata host.
*	BCT: Added prelude. Started test1 as a test of verification.	rustanleino	2010-05-12
\|
*	Moved BCT project references for Boogie to the Boogie\Binaries directory.	rustanleino	2010-04-16
\|
*	Upgraded solution file and project file to VS2010.	mikebarnett	2010-04-16
\|
*	Setting up test cases for BCT	schaef	2009-11-20
\|
*	Changed solution to include the CCI projects from Codeplex. (Still flaky in ↵	mikebarnett	2009-11-10
\| \| \| \|	that it assumes the CCI sources are in a particular relative location to the BCT sources.)
*	The beginnings of a CCI Metadata (http://ccimetadata.codeplex.com) based ↵	mikebarnett	2009-08-09
	bytecode translator.