| Commit message (Collapse) | Author | Age |
|
|
|
| |
Codeplex repositories.
|
|
|
|
|
|
| |
method calls are not followed by a test to see if an exception was thrown
"throw e" is translated as "assume false"
"try S catch C finally F" is translated as "S; F"
|
|
|
|
|
|
| |
heap monotonicity (and allocatedness of references
returned from a method) as well as the assert/assume
checks that are generated for every object dereference.
|
|
|
|
|
|
|
| |
it out for now) and used a simpler scheme for always
assigning compound bound expressions to a local.
Added the ability to assert/assume that an object is
non-null before dereferencing it.
|
|
|
|
| |
(like += or *=).
|
|
|
|
|
|
| |
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)
|
| |
|
| |
|
|
|
|
|
| |
of the struct value. This way it can do an allocation within the copy ctor
(if that is the design choice for structs, which it currently is).
|
|
|
|
| |
Define body for default struct ctors.
|
|
|
|
| |
the address is being taken.
|
|
|
|
| |
translated program in memory without writing it to disk.
|
|
|
|
| |
Boogie.
|
|
|
|
| |
Fixes for problems when translating generic type parameters.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
| |
initial value is getting allocated. Also, deferring ctor calls within a struct
ctor do *not* result in an attempt to allocate a new struct and assign it to
"this".
Restart the temporary variable counter on entry to each method. (This makes
the regressions less noisy because a change in the number of temporaries
created for one method will not change the names of the temporaries in other
methods.)
|
|
|
|
|
| |
the general heap uses.
Updated regressions.
|
| |
|
|
|
|
| |
BCT now links to CCI in CodeBox, get the CodeBox tree into C:\CCICodeBox
|
| |
|
|
|
|
| |
after each statement.
|
|
|
|
| |
If a method's parameters don't have names, give them names!
|
|
|
|
| |
members of a type can have the same name.
|
|
|
|
| |
inlining statistics
|
|
|
|
|
|
| |
assembly.
Fix in the Sink so that the consolidated index of a type parameter is computed
correctly.
|
|\ |
|
| |
| |
| |
| | |
assembly.
|
|/ |
|
| |
|
| |
|
| |
|
|
|
|
| |
Updated regression output due to Shaz's changes for exception handling.
|
|
|
|
| |
should be made into a plugin sometime
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
handle structs that call the default ctor on "this", translate conversion from
object to double, etc.
|
|
|
|
|
| |
is desired, then the CCI nodes must be created and an expression/statement
traverser used to translate it.
|
|
|
|
|
|
| |
that this means all methods with such parameters (where the parameter is passed
by value) must have free preconditions expressing that the parameters are
disjoint (since we are representing structs as Ref).
|
|
|
|
| |
that does the field-by-field copy.
|
|
|
|
|
| |
equality. Now each struct type has a default constructor that sets all of its
fields to zero-equivalent values.
|
|
|
|
|
|
|
|
|
| |
assemblies. This enables a translator to do whole-program analyses, such as
recording the subtype relationship across all of the input. (Still need to move
the delegate translation into this method.)
Fixed the existing whole-program translator so it uses the base class functionality
for translating the arguments to a method call.
Updated the regressions.
|
|
|
|
| |
ICreateObjectInstance.
|
|
|
|
|
|
| |
Normalize method bodies so anonymous delegates are gone.
Some attempts at simplifying.
New regression output.
|
| |
|
|
|
|
| |
new regression output.
|