summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator/TranslationHelper.cs
Commit message (Collapse)AuthorAge
* Removed the method DefaultValue from the sink: if a default value of a typeGravatar Mike Barnett2011-05-29
| | | | | is desired, then the CCI nodes must be created and an expression/statement traverser used to translate it.
* first cut at handling genericsGravatar qadeer2011-05-11
|
* Oops. Last checkin did not contain the changes for the catch clause change whenGravatar Mike Barnett2011-05-10
| | | | translating a method body.
* Uniquified constant names generated for string literalsGravatar qadeer2011-05-03
| | | | Also did some more substitutions to get valid Boogie identifiers
* bug fixes related to handling of structs, arrays, and assignmentsGravatar qadeer2011-05-02
|
* 0. Deleted other heap representations except SplitField and GeneralGravatar qadeer2011-04-23
| | | | 1. first cut at implementing structs
* changes for dealing with delegatesGravatar qadeer2011-03-05
|
* Made it unnecessary to set the types on the Boogie ASTs as we create them.Gravatar mikebarnett2011-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.
* implemented delegates and eventsGravatar qadeer2011-02-25
|
* Moved the creation of Boogie procedures from the MetadataTraverser to the ↵Gravatar mikebarnett2011-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.
* Fix the generation of procedure names so that array types are encoded properly.Gravatar mikebarnett2011-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.
* Added a better options parsing by using functionality from MemberHelper.Gravatar mikebarnett2011-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.
* Added a test for the split fields option.Gravatar mikebarnett2011-01-20
| | | | Refactored some code to make it easier to work with different heap representations.
* The beginning of the encapsulation of the Heap representation so that we can ↵Gravatar mikebarnett2011-01-17
| | | | easily have different ways of translating the heap.
* added support for array translation.Gravatar qadeer2010-12-20
|
* Translate boolean types into Bpl.Type.Bool.Gravatar mikebarnett2010-12-20
|
* Added Alloc implementation to the PreludeGravatar qadeer2010-12-15
| | | | | Fixed bug in translation of assume statement Added code for special handling of poirot specific calls
* Fixed field update and field dereference.Gravatar mikebarnett2010-12-09
|
* General hygiene: introduced (fixed) a helper method that creates Boogie ↵Gravatar mikebarnett2010-07-05
| | | | tokens. Made it an extension method that takes any object implementing IObjectWithLocations. Much easier to use within the translator.
* Cleaned up the sink: removed the OutVars, which was state the sink needed ↵Gravatar mikebarnett2010-07-05
| | | | only for assigning the local copy of a method's parameter to the out parameter of the Boogie procedure. But now that is simplified: instead of three versions of each parameter (in, local, and out), there are only two: in and out. For a parameter that is *not* by reference and is *not* an out parameter (i.e., just a plain pass-by-value parameter), the "out" version is a local variable. Otherwise it is an out parameter of the Boogie procedure.
* Forgotten file: Sink.csGravatar mikebarnett2010-07-05
| | | | Added an override of ToString so MethodParameters show up nicer in the debugger.
* Introduction of the Sink: a global object that is threaded through all of ↵Gravatar mikebarnett2010-07-02
| | | | the traversers and which contains the information that they need to share with each other.
* Updated the project to .NET v4.0.Gravatar mikebarnett2010-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.Gravatar rustanleino2010-05-12
|
* The beginnings of a CCI Metadata (http://ccimetadata.codeplex.com) based ↵Gravatar mikebarnett2009-08-09
bytecode translator.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 20:52:15 +0000