| Commit message (Expand) | Author | Age |
* | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codepl... | Rustan Leino | 2013-03-05 |
* | Moved the statement traverser's operand stack (used for explicit push/pop/dup | Unknown | 2012-09-09 |
* | Make the modelExceptions option an integer. | Unknown | 2012-08-22 |
* | Add an option to model exceptional control flow or not. When it is false: | Unknown | 2012-07-31 |
* | Added "free ensures" to procedures encoding the allocatedness | Unknown | 2012-04-10 |
* | Automated merge with https://hg01.codeplex.com/boogie | Mike Barnett | 2012-03-11 |
|\ |
|
* | | added breadcrumb to the beginning of each method | qadeer | 2012-03-09 |
| * | Automated merge with https://hg01.codeplex.com/boogie | Mike Barnett | 2012-02-27 |
|/| |
|
| * | Adapting to new decompiler. | Mike Barnett | 2012-02-27 |
* | | added :first attribute to the first line directive corresponding to a source ... | qadeer | 2012-02-13 |
|/ |
|
* | 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 |
* | | added another method that just throws an exception | qadeer | 2012-01-24 |
|/ |
|
* | Change the copy constructor for struct types so that it returns the copy | Mike Barnett | 2012-01-09 |
* | Add instrumentation for branches. | Mike Barnett | 2011-12-28 |
* | For some reason, these didn't get into the last commit. | Mike Barnett | 2011-11-14 |
* | Major changes to the translator traversers because they now are based on the | Mike Barnett | 2011-10-31 |
* | Fixed two bugs related to structs: now a struct that is declared without an | Mike Barnett | 2011-09-01 |
* | (bct) skeleton of plugin infrastructure. for now the code is essentially the ... | t-espave | 2011-08-16 |
* | Added option "getMeHere" so that calls to GetMeHere.Assert(e) become "assert e" | Mike Barnett | 2011-08-06 |
* | Added new option /captureState (/c) for generating a capture state assumption | Mike Barnett | 2011-08-04 |
* | refactored phonehelper | t-espave | 2011-07-28 |
* | ignoring (some) non-feedback producing event handlers | t-espave | 2011-07-26 |
* | weeding out non-set $exception as feedback handling issues | t-espave | 2011-07-26 |
* | updated translation of catch clauses to use Subtype | qadeer | 2011-07-20 |
* | edited out phoneplugin from most places | Unknown | 2011-07-19 |
* | Add a translation for switch statements. | Mike Barnett | 2011-07-14 |
* | implemented Mike's proposal for dynamic dispatch for finally blocks | qadeer | 2011-07-13 |
* | fixing exception translation according to discussion with mike | qadeer | 2011-07-13 |
* | ExtractLoops calls the same code for eliminating unreachable blocks that norm... | qadeer | 2011-07-05 |
* | 1. generating a separate dipatchcontinuation label for each trycatchfinally ... | qadeer | 2011-07-04 |
* | bug fix in translation of dispatch continuation | qadeer | 2011-06-23 |
* | Translate IConditional exactly the same way as IConditionalStatement to accou... | qadeer | 2011-06-20 |
* | various bug fixes related to running bct on phone apps | qadeer | 2011-06-12 |
* | further changes | qadeer | 2011-06-12 |
* | changes related to fixing problems with finally translation | qadeer | 2011-06-12 |
* | bunch of changes related to finally handling | qadeer | 2011-06-10 |
* | beginning support for finally clauses | qadeer | 2011-06-07 |
* | initial cut for translating exceptions | qadeer | 2011-06-06 |
* | Removed the method DefaultValue from the sink: if a default value of a type | Mike Barnett | 2011-05-29 |
* | Translate assignments of structs as a call to a (default) copy constructor | Mike Barnett | 2011-05-27 |
* | Beginning of representing structs as values on the heap, but without object | Mike Barnett | 2011-05-26 |
* | If a method has been translated as a function, generate a function call and | Mike Barnett | 2011-05-17 |
* | Merge | Mike Barnett | 2011-05-16 |
* | bug fixes related to handling of structs, arrays, and assignments | qadeer | 2011-05-02 |
* | The decompilation is not guaranteed to get rid of all push statements and pop | Mike Barnett | 2011-04-29 |
* | Changes needed to translate both contracts and method bodies. The Statement a... | mikebarnett | 2011-03-05 |
* | Made it unnecessary to set the types on the Boogie ASTs as we create them. | mikebarnett | 2011-03-03 |
* | Changed calls to Debug.Assert to Contract.Assert. | mikebarnett | 2011-02-24 |
* | Removed HeapVariable from everywhere now that it is encapsulated in the Heap ... | mikebarnett | 2011-01-19 |