summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator
Commit message (Collapse)AuthorAge
* 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.
* Forgotten file.Gravatar mikebarnett2010-06-30
|
* Simplified the translator by merging the ToplevelTraverser, ClassTraverser, ↵Gravatar mikebarnett2010-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 ↵Gravatar mikebarnett2010-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.
* Consistently use the new code pattern for translating locations to tokens ↵Gravatar mikebarnett2010-06-07
| | | | and putting the expression translation into a separate method.
* Added forgotten file.Gravatar mikebarnett2010-06-06
|
* 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
|
* Moved BCT project references for Boogie to the Boogie\Binaries directory.Gravatar rustanleino2010-04-16
|
* Upgraded solution file and project file to VS2010.Gravatar mikebarnett2010-04-16
|
* Updated to use new CCI API.Gravatar mikebarnett2010-04-16
|
* Setting up test cases for BCTGravatar schaef2009-11-20
|
* Update use of CCI's API for decompiling the IL model to the Code Model.Gravatar mikebarnett2009-11-17
|
* Changed solution to include the CCI projects from Codeplex. (Still flaky in ↵Gravatar mikebarnett2009-11-10
| | | | that it assumes the CCI sources are in a particular relative location to the BCT sources.)
* Changed error message to have correct program name.Gravatar mikebarnett2009-11-10
| | | | | Deleted custom host, just use the default host. Write output file to current directory, use "foo.bpl" as the output file name for the input assembly "foo".
* Please ignore. Just testing my account.Gravatar schaef2009-08-19
|
* 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-20 04:48:49 +0000