Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Change the copy constructor for struct types so that it returns the copy | 2012-01-09 | |
| | | | | | 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). | ||
* | Copy structs that are passed by value as method call arguments. | 2012-01-04 | |
| | | | | Define body for default struct ctors. | ||
* | For now, just ignore "address of" nodes and translate the expression of which | 2012-01-03 | |
| | | | | the address is being taken. | ||
* | Refactored translator so it can be called programmatically and return the | 2011-11-21 | |
| | | | | translated program in memory without writing it to disk. | ||
* | BCT: Initialize Boogie's command-line options object correctly before using | 2011-11-21 | |
| | | | | Boogie. | ||
* | Translate AddressOf expressions correctly. | 2011-11-16 | |
| | | | | Fixes for problems when translating generic type parameters. | ||
* | Many, many bug fixes related to generics and some other random problems. | 2011-11-10 | |
| | |||
* | Major changes to the translator traversers because they now are based on the | 2011-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. | ||
* | Fixed two bugs related to structs: now a struct that is declared without an | 2011-09-01 | |
| | | | | | | | | | | 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.) | ||
* | Made the split fields heap agree with the naming convention used for fields that | 2011-08-16 | |
| | | | | | the general heap uses. Updated regressions. | ||
* | Fixed problem where events in stubs were generating duplicate declarations. | 2011-08-11 | |
| | |||
* | (BCT) BREAKING CHANGE | 2011-08-11 | |
| | | | | BCT now links to CCI in CodeBox, get the CodeBox tree into C:\CCICodeBox | ||
* | (phone bct) nav graph building (mostly) automated | 2011-08-05 | |
| | |||
* | Added new option /captureState (/c) for generating a capture state assumption | 2011-08-04 | |
| | | | | after each statement. | ||
* | Changed name mangling (again) to avoid name clashes. | 2011-08-04 | |
| | | | | If a method's parameters don't have names, give them names! | ||
* | Increase the name mangling to avoid name clashes in the Boogie program. In IL, | 2011-08-03 | |
| | | | | members of a type can have the same name. | ||
* | (phone bct) default URI checks inlined | 2011-08-02 | |
| | | | | inlining statistics | ||
* | Fix in the assertion injector for putting the output on top of the input | 2011-08-01 | |
| | | | | | | assembly. Fix in the Sink so that the consolidated index of a type parameter is computed correctly. | ||
* | Merge | 2011-07-27 | |
|\ | |||
* | | Implemented a whitelist/blacklist so translator can ignore certain parts of an | 2011-07-27 | |
| | | | | | | | | assembly. | ||
| * | fixed right/left shift functions decl | 2011-07-27 | |
|/ | |||
* | Updated regressions. | 2011-07-27 | |
| | |||
* | adding checks and code injection for phone feedback checking | 2011-07-25 | |
| | |||
* | Added subtyping axiomatization. | 2011-07-20 | |
| | |||
* | Add a translation for switch statements. | 2011-07-14 | |
| | | | | Updated regression output due to Shaz's changes for exception handling. | ||
* | phone control exploration for BCT, not integrated yet | 2011-07-07 | |
| | | | | should be made into a plugin sometime | ||
* | Updated regression output. | 2011-07-06 | |
| | |||
* | Updated regression output. | 2011-07-06 | |
| | |||
* | Fixed/improved the handling of conditional expressions. | 2011-05-31 | |
| | |||
* | Added bitwise operations. | 2011-05-31 | |
| | |||
* | Lots of small bug fixes: conversions, overloaded operations on real numbers. | 2011-05-31 | |
| | |||
* | Handle more conversions. | 2011-05-29 | |
| | |||
* | Fixes for a bunch of different bugs. Translate default value for doubles, | 2011-05-29 | |
| | | | | | handle structs that call the default ctor on "this", translate conversion from object to double, etc. | ||
* | Removed the method DefaultValue from the sink: if a default value of a type | 2011-05-29 | |
| | | | | | is desired, then the CCI nodes must be created and an expression/statement traverser used to translate it. | ||
* | Translate assignments to parameters that are of a struct type correctly. Note | 2011-05-28 | |
| | | | | | | 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). | ||
* | Translate assignments of structs as a call to a (default) copy constructor | 2011-05-27 | |
| | | | | that does the field-by-field copy. | ||
* | Beginning of representing structs as values on the heap, but without object | 2011-05-26 | |
| | | | | | equality. Now each struct type has a default constructor that sets all of its fields to zero-equivalent values. | ||
* | Created an API so that a MetadataTraverser is used to translate a set of | 2011-05-21 | |
| | | | | | | | | | 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. | ||
* | Unify translation of arguments so the same code is used for IMethodCall and | 2011-05-19 | |
| | | | | ICreateObjectInstance. | ||
* | Add extern declarations to procedures. | 2011-05-16 | |
| | | | | | | Normalize method bodies so anonymous delegates are gone. Some attempts at simplifying. New regression output. | ||
* | Trying to fix the bound expression simplifier. | 2011-05-12 | |
| | |||
* | Cleanup of new LHS simplification and replaced the golden output with the | 2011-05-06 | |
| | | | | new regression output. | ||
* | The decompilation is not guaranteed to get rid of all push statements and pop | 2011-04-29 | |
| | | | | | | expressions. So added support for them. Simplified the API in the sink for creating a local. Not it takes a CCI type so clients do not have to first translate the CCI type to the Boogie type. | ||
* | Model newly constructed structs as a constant DefaultStruct that has axioms that | 2011-04-27 | |
| | | | | define it to return zero-equivalent values for all fields. | ||
* | merge changes with shaz's checkin. | 2011-04-27 | |
|\ | |||
| * | Trying to get structs supported. | 2011-04-27 | |
| | | |||
* | | fixes to struct translation | 2011-04-27 | |
|/ | |||
* | 0. Deleted other heap representations except SplitField and General | 2011-04-23 | |
| | | | | 1. first cut at implementing structs | ||
* | Fix stub support (still not completely finished). | 2011-04-12 | |
| | | | | | | Fix generation of delegate methods so that they happen after translating all input assemblies and not per assembly. Fix translation of typeof() expressions. | ||
* | More support for stubs. Ability to add functions as well as procedures. | 2011-04-04 | |
| |