| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Find implementations of interface methods for dynamic dispatch, not just |  Unknown | 2012-09-09 |
| | | | | | overrides of virtual methods. | ||
| * | Avoid creating a dynamic dispatch table for GetHashCode and ToString: it ends | Unknown | 2012-09-09 |
| | | | | | | up creating code that the Boogie parser gets a stack overflow while trying to parse! | ||
| * | Moved the statement traverser's operand stack (used for explicit push/pop/dup | Unknown | 2012-09-09 |
| | | | | | | | | | | | in the code model) into the sink so that the different statement traversers used for things like if-then-else statements share the same stack. Fixed a problem in the dispatch table for whole program virtual dispatch so it works for generic methods. Found input that either crashed the translator or caused it to produce bad Boogie: "fixed" it by having the translator thrown an exception so the method containing the bad code is skipped. | ||
| * | Fix the whole-program translator so that exception handling is done | Unknown | 2012-08-23 |
| | | | | | | | | | | | correctly for virtual method calls. Changed the whole-program override for VisitMethodCall so that it creates a new CodeModel expression that does not contain virtual method calls and then translate that newly built expression. Treat type equality (and inequality) specially: translate it directly to a type test instead. But do it just for the idiom: "o.GetType == typeof(T)". In that case, turn it into "is#T$T($DynamicType(o))". | ||
| * | Make the modelExceptions option an integer. | Unknown | 2012-08-22 |
| | | | | | | | | | | | | | | | | 0 means no modeling at all. 1 (which can be specified only if also specifying whole program translation) means that a fixpoint analysis will be done on all of the translated assemblies to compute the set of exceptions that each method can throw (even though we're using only the fact that a method throws anything at all, not the specific exceptions it can throw) so only calls to methods that can throw an exception have a branch after the call that checks to see if an exception has been thrown. Methods that are defined outside of the set of translated assemblies are assumed to *not* throw any exceptions! 2 means that every method is considered to be one that can throw an exception. | ||
| * | Fix a bug when static fields are used in as operands for ++ or --. | Unknown | 2012-07-31 |
| | | |||
| * | Add an option to model exceptional control flow or not. When it is false: | Unknown | 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 | Unknown | 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 | Unknown | 2012-06-02 |
| | | | | | to be translated. | ||
| * | Fix for addressof expressions. | Unknown | 2012-05-18 |
| | | |||
| * | Add options to control the emission of free ensures for | Unknown | 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 | Unknown | 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 | Unknown | 2012-04-10 |
| | | | | | of references. | ||
| * | Fix a lot of the translation of "op=" expressions | Unknown | 2012-04-09 |
| | | | | | (like += or *=). | ||
| * | Changed the BCT solution so it uses the CodePlex version of CCI (instead |  Mike Barnett | 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 | Mike Barnett | 2012-03-29 |
| |\ | |||
| * | | updated Boogie strings so that they can refer to \" (and more) |  qadeer | 2012-03-12 |
| | | | | | | | | | fixed BCT :value | ||
| | * | Automated merge with https://hg01.codeplex.com/boogie | Mike Barnett | 2012-03-11 |
| |/| | |||
| | * | more work on op-assign expressions. (unfinished) | Mike Barnett | 2012-03-11 |
| | | | |||
| * | | further sanitization of string in :value attribute | qadeer | 2012-03-11 |
| | | | |||
| * | | added breadcrumb to the beginning of each method | qadeer | 2012-03-09 |
| | | | |||
| * | | value attribute "\n" to "\\n" | qadeer | 2012-03-01 |
| | | | | | | | | | more work is perhaps needed to handle all cases | ||
| | * | Automated merge with https://hg01.codeplex.com/boogie | Mike Barnett | 2012-02-27 |
| |/| | |||
| | * | Adapting to new decompiler. | Mike Barnett | 2012-02-27 |
| | | | | | | | | | Dynamic dispatch for interface method calls. | ||
| * | | adding attribute for string literals |  qadeer | 2012-02-27 |
| | | | |||
| * | | added :first attribute to the first line directive corresponding to a source ↵ | qadeer | 2012-02-13 |
| |/ | | | | line | ||
| * | Union is now based on axioms | qadeer | 2012-02-07 |
| | | | | | added more inline attributes | ||
| * | fixed bug in model parsing | qadeer | 2012-02-06 |
| | | | | | converted a bunch of definitions to be inlined | ||
| * | Merge | qadeer | 2012-02-06 |
| |\ | |||
| * | | added inlining support for all implementations given the attribute {:inline 1} | qadeer | 2012-02-06 |
| | | | | | | | | | | | removed AssertionInjector from the solution changed the representation of multicast delegates | ||
| | * | Automated merge with https://hg01.codeplex.com/boogie | Mike Barnett | 2012-02-05 |
| |/| | |||
| | * | Separated the concepts of "boxing" (i.e., CLR boxing of a value type) from | Mike Barnett | 2012-02-05 |
| | | | | | | | | | the "union" type that is the supertype of all the translated Boogie types. | ||
| * | | added a dummy sourceLine attribute for delegate dispatch | qadeer | 2012-01-31 |
| | | | |||
| * | | added another project | qadeer | 2012-01-30 |
| | | | |||
| | * | Automated merge with https://hg01.codeplex.com/boogie | Mike Barnett | 2012-01-26 |
| | |\ | |||
| | | * | Separate out the concepts of boxing | Mike Barnett | 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 | qadeer | 2012-01-24 |
| |/ / | |||
| * / | an optimization in dynamic dispatch | qadeer | 2012-01-23 |
| |/ | | | | a hack in event translation | ||
| * | Mark the procedure translated from the module's entry point | Mike Barnett | 2012-01-15 |
| | | | | | with the attribute {:entrypoint}. | ||
| * | Make a copy of a struct value being passed to a method | Mike Barnett | 2012-01-10 |
| | | | | | whether the method is generic or not. | ||
| * | Fix call to struct copy ctor. | Mike Barnett | 2012-01-10 |
| | | |||
| * | Fixed struct copy constructor implementation. | Mike Barnett | 2012-01-10 |
| | | |||
| * | Change the copy constructor for struct types so that it returns the copy | Mike Barnett | 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. | Mike Barnett | 2012-01-04 |
| | | | | | Define body for default struct ctors. | ||
| * | For now, just ignore "address of" nodes and translate the expression of which | Mike Barnett | 2012-01-03 |
| | | | | | the address is being taken. | ||
| * | new axioms for subtyping | qadeer | 2011-12-31 |
| | | |||
| * | modeling multiset using generalized array theory | qadeer | 2011-12-30 |
| | | |||
| * | made delegate a datatype | qadeer | 2011-12-30 |
| | | | | | added a DatatypeConstructor class | ||
| * | problem fixed after CCI update | qadeer | 2011-12-30 |
| | | |||
| * | fixed problems with datatypes | qadeer | 2011-12-29 |
| | | | | | | removed stale contracts in stratified inlining added test to datatypes | ||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |