summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator/StatementTraverser.cs
Commit message (Expand)AuthorAge
* Removed the method DefaultValue from the sink: if a default value of a typeGravatar Mike Barnett2011-05-29
* Translate assignments of structs as a call to a (default) copy constructorGravatar Mike Barnett2011-05-27
* Beginning of representing structs as values on the heap, but without objectGravatar Mike Barnett2011-05-26
* If a method has been translated as a function, generate a function call andGravatar Mike Barnett2011-05-17
* MergeGravatar Mike Barnett2011-05-16
* bug fixes related to handling of structs, arrays, and assignmentsGravatar qadeer2011-05-02
* The decompilation is not guaranteed to get rid of all push statements and popGravatar Mike Barnett2011-04-29
* Changes needed to translate both contracts and method bodies. The Statement a...Gravatar mikebarnett2011-03-05
* Made it unnecessary to set the types on the Boogie ASTs as we create them.Gravatar mikebarnett2011-03-03
* Changed calls to Debug.Assert to Contract.Assert.Gravatar mikebarnett2011-02-24
* Removed HeapVariable from everywhere now that it is encapsulated in the Heap ...Gravatar mikebarnett2011-01-19
* 1. Converted assume to assert for the source infoGravatar qadeer2010-12-21
* Changed attribute names in the BPL for source context assumption statements.Gravatar mikebarnett2010-12-21
* Use an explicit PdbReader instead of the more general ISourceLocationProvider...Gravatar mikebarnett2010-12-21
* added support for array translation.Gravatar qadeer2010-12-20
* Generate "assume {:filename "foo.cs"}{:line 3} true" statements for each stat...Gravatar mikebarnett2010-12-20
* Added Alloc implementation to the PreludeGravatar qadeer2010-12-15
* General hygiene: introduced (fixed) a helper method that creates Boogie token...Gravatar mikebarnett2010-07-05
* Cleaned up the sink: removed the OutVars, which was state the sink needed onl...Gravatar mikebarnett2010-07-05
* Introduction of the Sink: a global object that is threaded through all of the...Gravatar mikebarnett2010-07-02
* Simplified the translator by merging the ToplevelTraverser, ClassTraverser, a...Gravatar mikebarnett2010-06-28
* Added the factory pattern so that all traversers are created through factory ...Gravatar mikebarnett2010-06-16
* Consistently use the new code pattern for translating locations to tokens and...Gravatar mikebarnett2010-06-07
* Updated the project to .NET v4.0.Gravatar mikebarnett2010-06-06
* The beginnings of a CCI Metadata (http://ccimetadata.codeplex.com) based byte...Gravatar mikebarnett2009-08-09