| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
tokens. Made it an extension method that takes any object implementing IObjectWithLocations. Much easier to use within the translator.
|
| |
|
|
| |
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.
|
| |
|
|
| |
Added an override of ToString so MethodParameters show up nicer in the debugger.
|
| |
|
|
| |
the traversers and which contains the information that they need to share with each other.
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
| |
and putting the expression translation into a separate method.
|
| | |
|
| |
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
that it assumes the CCI sources are in a particular relative location to the BCT sources.)
|
| |
|
|
|
| |
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".
|
| | |
|
|
|
bytecode translator.
|
mikebarnett