summaryrefslogtreecommitdiff
path: root/BCT/RegressionTests
Commit message (Collapse)AuthorAge
* Add an option to model exceptional control flow or not. When it is false:Gravatar Unknown2012-07-31
| | | | | | 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"
* Add options to control the emission of free ensures forGravatar Unknown2012-04-16
| | | | | | heap monotonicity (and allocatedness of references returned from a method) as well as the assert/assume checks that are generated for every object dereference.
* Removed expression simplifier (actually just commentedGravatar Unknown2012-04-15
| | | | | | | 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.
* Fix a lot of the translation of "op=" expressionsGravatar Unknown2012-04-09
| | | | (like += or *=).
* Changed the BCT solution so it uses the CodePlex version of CCI (insteadGravatar Mike Barnett2012-03-30
| | | | | | 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)
* Fix call to struct copy ctor.Gravatar Mike Barnett2012-01-10
|
* Fixed struct copy constructor implementation.Gravatar Mike Barnett2012-01-10
|
* Change the copy constructor for struct types so that it returns the copyGravatar Mike Barnett2012-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.Gravatar Mike Barnett2012-01-04
| | | | Define body for default struct ctors.
* For now, just ignore "address of" nodes and translate the expression of whichGravatar Mike Barnett2012-01-03
| | | | the address is being taken.
* Refactored translator so it can be called programmatically and return theGravatar Mike Barnett2011-11-21
| | | | translated program in memory without writing it to disk.
* BCT: Initialize Boogie's command-line options object correctly before usingGravatar Mike Barnett2011-11-21
| | | | Boogie.
* Translate AddressOf expressions correctly.Gravatar Mike Barnett2011-11-16
| | | | Fixes for problems when translating generic type parameters.
* 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
| | | | | | | | 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 anGravatar Mike Barnett2011-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 thatGravatar Mike Barnett2011-08-16
| | | | | the general heap uses. Updated regressions.
* Fixed problem where events in stubs were generating duplicate declarations.Gravatar Mike Barnett2011-08-11
|
* (BCT) BREAKING CHANGEGravatar t-espave2011-08-11
| | | | BCT now links to CCI in CodeBox, get the CodeBox tree into C:\CCICodeBox
* (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
| | | | after each statement.
* Changed name mangling (again) to avoid name clashes.Gravatar Mike Barnett2011-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,Gravatar Mike Barnett2011-08-03
| | | | members of a type can have the same name.
* (phone bct) default URI checks inlinedGravatar t-espave2011-08-02
| | | | inlining statistics
* Fix in the assertion injector for putting the output on top of the inputGravatar Mike Barnett2011-08-01
| | | | | | assembly. Fix in the Sink so that the consolidated index of a type parameter is computed correctly.
* MergeGravatar Mike Barnett2011-07-27
|\
* | Implemented a whitelist/blacklist so translator can ignore certain parts of anGravatar Mike Barnett2011-07-27
| | | | | | | | assembly.
| * 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
| | | | Updated regression output due to Shaz's changes for exception handling.
* phone control exploration for BCT, not integrated yetGravatar Unknown2011-07-07
| | | | should be made into a plugin sometime
* 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
| | | | | 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 typeGravatar Mike Barnett2011-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. NoteGravatar Mike Barnett2011-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 constructorGravatar Mike Barnett2011-05-27
| | | | that does the field-by-field copy.
* Beginning of representing structs as values on the heap, but without objectGravatar Mike Barnett2011-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 ofGravatar Mike Barnett2011-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 andGravatar Mike Barnett2011-05-19
| | | | ICreateObjectInstance.
* Add extern declarations to procedures.Gravatar Mike Barnett2011-05-16
| | | | | | Normalize method bodies so anonymous delegates are gone. Some attempts at simplifying. New regression output.
* 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
| | | | new regression output.
* The decompilation is not guaranteed to get rid of all push statements and popGravatar Mike Barnett2011-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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:24:05 +0000