| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Codeplex repositories.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
0 means no modeling at all.
1 (which can be specified only if also specifying whole program translation)
means that a fixpoint analysis will be done on all of the translated assemblies
to compute the set of exceptions that each method can throw (even though we're
using only the fact that a method throws anything at all, not the specific
exceptions it can throw) so only calls to methods that can throw an exception
have a branch after the call that checks to see if an exception has been
thrown. Methods that are defined outside of the set of translated assemblies
are assumed to *not* throw any exceptions!
2 means that every method is considered to be one that can throw an exception.
|
| |
|
|
|
|
| |
of the internal version).
Fixed the expression traverser to (begin the) support target expressions as
operands of binary expressions. (e.g., x++ or x += 2)
|
| |
|
|
| |
Dynamic dispatch for interface method calls.
|
| |
|
|
|
|
| |
same
I will open a plugin branch to make more deeper changes until everything is stable
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
reported at end of analysis
|
| |
|
|
| |
BCT now links to CCI in CodeBox, get the CodeBox tree into C:\CCICodeBox
|
| |
|
|
| |
back key handling code not reflected in nav graph - usually the programmer's intent
|
| |
|
|
| |
analysis)
|
| | |
|
| |
|
|
| |
- injecting navigation changes code
|
| |
|
|
| |
- (some) URI declaration/instantiation and use detection
|
| | |
|
| |
|
|
| |
should be made into a plugin sometime
|
| | |
|
| |
|
|
|
| |
Suppress source contexts for empty statements.
Added a "whole program" option. When that is specified, then virtual calls are translated into a series of if-statements that test the dynamic type of the receiver and call the appropriate method. This is done only for subtypes that are defined in the CUA (Code Under Analysis -- which currently consists of just the one assembly being translated). [Note: currently the dynamic type is not implemented. That is next.]
|
| |
|
|
| |
representation is implemented as a different object.
|
| |
|
|
| |
easily have different ways of translating the heap.
|
| |
|
|
| |
moved into that assembly.
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
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.)
|
|
|
bytecode translator.
|
Rustan Leino
Unknown
Mike Barnett
qadeer
Unknown