index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
BCT
/
BytecodeTranslator
/
StatementTraverser.cs
Commit message (
Expand
)
Author
Age
*
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
*
1. Converted assume to assert for the source info
qadeer
2010-12-21
*
Changed attribute names in the BPL for source context assumption statements.
mikebarnett
2010-12-21
*
Use an explicit PdbReader instead of the more general ISourceLocationProvider...
mikebarnett
2010-12-21
*
added support for array translation.
qadeer
2010-12-20
[next]