summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator/TranslationHelper.cs
Commit message (Collapse)AuthorAge
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵Gravatar Rustan Leino2013-03-05
| | | | Codeplex repositories.
* Trying to get the generics translation correct...Gravatar Mike Barnett2011-11-14
|
* Many, many bug fixes related to generics and some other random problems.Gravatar Mike Barnett2011-11-10
|
* Major changes to the translator traversers because they now are based on theGravatar Mike Barnett2011-10-31
| | | | | | | | new traversers. (The old ones have been marked as obsolete.) All types are now encoded as "datatypes" in Boogie. So non-generic types are nullary functions and generic types just have at least one type argument. Lots of other fixes: string encoding of names is now done by negating Boogie's regular expression for identifiers, etc.
* more string manglingGravatar qadeer2011-08-31
|
* MergeGravatar qadeer2011-08-26
|\
* | some more string mungingGravatar qadeer2011-08-26
| |
| * (bct) removed ad-hoc string replacements, the problem is actually the encodingGravatar t-espave2011-08-25
|/
* (phone bct) minor bugfixes found playing around with appsGravatar t-espave2011-08-19
|
* various fixes to deal with bug in generic delegatesGravatar qadeer2011-08-12
|
* (phone bct) nav graph building (mostly) automatedGravatar t-espave2011-08-05
|
* MergeGravatar t-espave2011-08-04
|\
| * Changed name mangling (again) to avoid name clashes.Gravatar Mike Barnett2011-08-04
| | | | | | | | If a method's parameters don't have names, give them names!
* | MergeGravatar t-espave2011-08-03
|\|
| * Increase the name mangling to avoid name clashes in the Boogie program. In IL,Gravatar Mike Barnett2011-08-03
| | | | | | | | members of a type can have the same name.
* | (phone bct) user feedback, showing possibly anomalous nav targetsGravatar t-espave2011-08-03
|/ | | | (bct) '+' invalid in string literals
* Unicode surrogate characters cannot be handled by Boogie. For now (forever?)Gravatar Mike Barnett2011-08-02
| | | | just delete them from the identifier that represents each literal string.
* various bug fixes related to running bct on phone appsGravatar qadeer2011-06-12
|
* changes related to fixing problems with finally translationGravatar qadeer2011-06-12
|
* beginning support for finally clausesGravatar qadeer2011-06-07
|
* initial cut for translating exceptionsGravatar qadeer2011-06-06
|
* Lots of small bug fixes: conversions, overloaded operations on real numbers.Gravatar Mike Barnett2011-05-31
|
* Fixed struct ctors so that they don't return the "this" value, but justGravatar Mike Barnett2011-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.
* 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.