summaryrefslogtreecommitdiff
path: root/BCT/RegressionTests/TranslationTest
Commit message (Expand)AuthorAge
* Add options to control the emission of free ensures forGravatar Unknown2012-04-16
* Removed expression simplifier (actually just commentedGravatar Unknown2012-04-15
* Fix a lot of the translation of "op=" expressionsGravatar Unknown2012-04-09
* Changed the BCT solution so it uses the CodePlex version of CCI (insteadGravatar Mike Barnett2012-03-30
* Fix call to struct copy ctor.Gravatar Mike Barnett2012-01-10
* Change the copy constructor for struct types so that it returns the copyGravatar Mike Barnett2012-01-09
* Copy structs that are passed by value as method call arguments.Gravatar Mike Barnett2012-01-04
* For now, just ignore "address of" nodes and translate the expression of whichGravatar Mike Barnett2012-01-03
* Refactored translator so it can be called programmatically and return theGravatar Mike Barnett2011-11-21
* BCT: Initialize Boogie's command-line options object correctly before usingGravatar Mike Barnett2011-11-21
* Translate AddressOf expressions correctly.Gravatar Mike Barnett2011-11-16
* Many, many bug fixes related to generics and some other random problems.Gravatar Mike Barnett2011-11-10
* Major changes to the translator traversers because they now are based on theGravatar Mike Barnett2011-10-31
* Fixed two bugs related to structs: now a struct that is declared without anGravatar Mike Barnett2011-09-01
* Made the split fields heap agree with the naming convention used for fields thatGravatar Mike Barnett2011-08-16
* Fixed problem where events in stubs were generating duplicate declarations.Gravatar Mike Barnett2011-08-11
* (BCT) BREAKING CHANGEGravatar t-espave2011-08-11
* (phone bct) nav graph building (mostly) automatedGravatar t-espave2011-08-05
* Added new option /captureState (/c) for generating a capture state assumptionGravatar Mike Barnett2011-08-04
* Changed name mangling (again) to avoid name clashes.Gravatar Mike Barnett2011-08-04
* Increase the name mangling to avoid name clashes in the Boogie program. In IL,Gravatar Mike Barnett2011-08-03
* (phone bct) default URI checks inlinedGravatar t-espave2011-08-02
* Fix in the assertion injector for putting the output on top of the inputGravatar Mike Barnett2011-08-01
* MergeGravatar Mike Barnett2011-07-27
|\
* | Implemented a whitelist/blacklist so translator can ignore certain parts of anGravatar Mike Barnett2011-07-27
| * fixed right/left shift functions declGravatar t-espave2011-07-27
|/
* Updated regressions.Gravatar Mike Barnett2011-07-27
* adding checks and code injection for phone feedback checkingGravatar t-espave2011-07-25
* Added subtyping axiomatization.Gravatar Mike Barnett2011-07-20
* Add a translation for switch statements.Gravatar Mike Barnett2011-07-14
* phone control exploration for BCT, not integrated yetGravatar Unknown2011-07-07
* Updated regression output.Gravatar Mike Barnett2011-07-06
* Updated regression output.Gravatar Mike Barnett2011-07-06
* Fixed/improved the handling of conditional expressions.Gravatar Mike Barnett2011-05-31
* Added bitwise operations.Gravatar Mike Barnett2011-05-31
* Lots of small bug fixes: conversions, overloaded operations on real numbers.Gravatar Mike Barnett2011-05-31
* Handle more conversions.Gravatar Mike Barnett2011-05-29
* Fixes for a bunch of different bugs. Translate default value for doubles,Gravatar Mike Barnett2011-05-29
* Removed the method DefaultValue from the sink: if a default value of a typeGravatar Mike Barnett2011-05-29
* Translate assignments to parameters that are of a struct type correctly. NoteGravatar Mike Barnett2011-05-28
* Translate assignments of structs as a call to a (default) copy constructorGravatar Mike Barnett2011-05-27
* Beginning of representing structs as values on the heap, but without objectGravatar Mike Barnett2011-05-26
* Created an API so that a MetadataTraverser is used to translate a set ofGravatar Mike Barnett2011-05-21
* Unify translation of arguments so the same code is used for IMethodCall andGravatar Mike Barnett2011-05-19
* Add extern declarations to procedures.Gravatar Mike Barnett2011-05-16
* Trying to fix the bound expression simplifier.Gravatar Mike Barnett2011-05-12
* Cleanup of new LHS simplification and replaced the golden output with theGravatar Mike Barnett2011-05-06
* The decompilation is not guaranteed to get rid of all push statements and popGravatar Mike Barnett2011-04-29
* Model newly constructed structs as a constant DefaultStruct that has axioms thatGravatar Unknown2011-04-27
* fixes to struct translationGravatar qadeer2011-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 07:34:13 +0000