Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix a bug when static fields are used in as operands for ++ or --. | 2012-07-31 | |
| | |||
* | Add an option to model exceptional control flow or not. When it is false: | 2012-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" | ||
* | When translating an assighment, leave the source of the assignment on the | 2012-06-02 | |
| | | | | stack in case it is needed by an enclosing expression. | ||
* | Don't add dummy modules (resulting from a failed load) to the list of modules | 2012-06-02 | |
| | | | | to be translated. | ||
* | Fix for addressof expressions. | 2012-05-18 | |
| | |||
* | Add options to control the emission of free ensures for | 2012-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 commented | 2012-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. | ||
* | Added "free ensures" to procedures encoding the allocatedness | 2012-04-10 | |
| | | | | of references. | ||
* | Fix a lot of the translation of "op=" expressions | 2012-04-09 | |
| | | | | (like += or *=). | ||
* | Changed the BCT solution so it uses the CodePlex version of CCI (instead | 2012-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) | ||
* | Automated merge with https://hg01.codeplex.com/boogie | 2012-03-29 | |
|\ | |||
* | | updated Boogie strings so that they can refer to \" (and more) | 2012-03-12 | |
| | | | | | | | | fixed BCT :value | ||
| * | Automated merge with https://hg01.codeplex.com/boogie | 2012-03-11 | |
|/| | |||
| * | more work on op-assign expressions. (unfinished) | 2012-03-11 | |
| | | |||
* | | further sanitization of string in :value attribute | 2012-03-11 | |
| | | |||
* | | added breadcrumb to the beginning of each method | 2012-03-09 | |
| | | |||
* | | value attribute "\n" to "\\n" | 2012-03-01 | |
| | | | | | | | | more work is perhaps needed to handle all cases | ||
| * | Automated merge with https://hg01.codeplex.com/boogie | 2012-02-27 | |
|/| | |||
| * | Adapting to new decompiler. | 2012-02-27 | |
| | | | | | | | | Dynamic dispatch for interface method calls. | ||
* | | adding attribute for string literals | 2012-02-27 | |
| | | |||
* | | added :first attribute to the first line directive corresponding to a source ↵ | 2012-02-13 | |
|/ | | | | line | ||
* | Union is now based on axioms | 2012-02-07 | |
| | | | | added more inline attributes | ||
* | fixed bug in model parsing | 2012-02-06 | |
| | | | | converted a bunch of definitions to be inlined | ||
* | Merge | 2012-02-06 | |
|\ | |||
* | | added inlining support for all implementations given the attribute {:inline 1} | 2012-02-06 | |
| | | | | | | | | | | removed AssertionInjector from the solution changed the representation of multicast delegates | ||
| * | Automated merge with https://hg01.codeplex.com/boogie | 2012-02-05 | |
|/| | |||
| * | Separated the concepts of "boxing" (i.e., CLR boxing of a value type) from | 2012-02-05 | |
| | | | | | | | | the "union" type that is the supertype of all the translated Boogie types. | ||
* | | added a dummy sourceLine attribute for delegate dispatch | 2012-01-31 | |
| | | |||
* | | added another project | 2012-01-30 | |
| | | |||
| * | Automated merge with https://hg01.codeplex.com/boogie | 2012-01-26 | |
| |\ | |||
| | * | Separate out the concepts of boxing | 2012-01-26 | |
| | | | | | | | | | | | | | | | | | | | | | (i.e., CLR's creating a heap cell and putting a value into it) from the concept of the "union" type that all Boogie types are a subtype of. | ||
* | | | added another method that just throws an exception | 2012-01-24 | |
|/ / | |||
* / | an optimization in dynamic dispatch | 2012-01-23 | |
|/ | | | | a hack in event translation | ||
* | Mark the procedure translated from the module's entry point | 2012-01-15 | |
| | | | | with the attribute {:entrypoint}. | ||
* | Make a copy of a struct value being passed to a method | 2012-01-10 | |
| | | | | whether the method is generic or not. | ||
* | Fix call to struct copy ctor. | 2012-01-10 | |
| | |||
* | Fixed struct copy constructor implementation. | 2012-01-10 | |
| | |||
* | 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. | ||
* | new axioms for subtyping | 2011-12-31 | |
| | |||
* | modeling multiset using generalized array theory | 2011-12-30 | |
| | |||
* | made delegate a datatype | 2011-12-30 | |
| | | | | added a DatatypeConstructor class | ||
* | problem fixed after CCI update | 2011-12-30 | |
| | |||
* | fixed problems with datatypes | 2011-12-29 | |
| | | | | | removed stale contracts in stratified inlining added test to datatypes | ||
* | Merge | 2011-12-28 | |
|\ | |||
* | | deleted some commented code | 2011-12-28 | |
| | | |||
| * | Add instrumentation for branches. | 2011-12-28 | |
|/ | |||
* | refactored AssertionInjector so that it works directly on bpl files as well | 2011-12-26 | |
| | |||
* | bug fix in houdini inlineDepth | 2011-12-06 | |
| |