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
/
Sink.cs
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 options to control the emission of free ensures for
Unknown
2012-04-16
*
Added "free ensures" to procedures encoding the allocatedness
Unknown
2012-04-10
*
updated Boogie strings so that they can refer to \" (and more)
qadeer
2012-03-12
*
further sanitization of string in :value attribute
qadeer
2012-03-11
*
value attribute "\n" to "\\n"
qadeer
2012-03-01
*
adding attribute for string literals
qadeer
2012-02-27
*
Merge
qadeer
2012-02-06
|
\
*
|
added inlining support for all implementations given the attribute {:inline 1}
qadeer
2012-02-06
|
*
Separate out the concepts of boxing
Mike Barnett
2012-01-26
|
/
*
Change the copy constructor for struct types so that it returns the copy
Mike Barnett
2012-01-09
*
Copy structs that are passed by value as method call arguments.
Mike Barnett
2012-01-04
*
new axioms for subtyping
qadeer
2011-12-31
*
Translate AddressOf expressions correctly.
Mike Barnett
2011-11-16
*
Load all assemblies before doing anything else so that the unification for
Mike Barnett
2011-11-16
*
Trying to get the generics translation correct...
Mike Barnett
2011-11-14
*
Many, many bug fixes related to generics and some other random problems.
Mike Barnett
2011-11-10
*
Don't wipe out existing attributes when adding {:extern}
Mike Barnett
2011-11-01
*
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
*
delegates/events implemented as multisets rather than linked lists
qadeer
2011-08-30
*
fixed a bug: do not include the invoke procedure for thread delegates in the ...
qadeer
2011-08-25
*
(bct) skeleton of plugin infrastructure. for now the code is essentially the ...
t-espave
2011-08-16
*
Merge
qadeer
2011-08-11
|
\
*
|
fixes for bug with generic delegates
qadeer
2011-08-11
|
*
Fixed problem where events in stubs were generating duplicate declarations.
Mike Barnett
2011-08-11
|
/
*
Merge
t-espave
2011-08-08
|
\
|
*
another bug fix in bct
qadeer
2011-08-08
|
*
added a new file and fixed a bug in bct
qadeer
2011-08-08
|
/
*
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
*
Increase the name mangling to avoid name clashes in the Boogie program. In IL,
Mike Barnett
2011-08-03
*
Fix in the assertion injector for putting the output on top of the input
Mike Barnett
2011-08-01
*
Implemented a whitelist/blacklist so translator can ignore certain parts of an
Mike Barnett
2011-07-27
*
weeding out non-set $exception as feedback handling issues
t-espave
2011-07-26
*
Added subtyping axiomatization.
Mike Barnett
2011-07-20
*
edited out phoneplugin from most places
Unknown
2011-07-19
*
commenting out axiom generation
qadeer
2011-07-15
*
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
*
phone injecting code traverser
Unknown
2011-07-08
*
Merge
Mike Barnett
2011-07-08
|
\
*
|
Fix translation of "is" operator.
Mike Barnett
2011-07-08
|
*
phone control exploration for BCT, not integrated yet
Unknown
2011-07-07
|
/
*
Beginning of encoding the subtype relation.
Mike Barnett
2011-07-06
*
Merge
Mike Barnett
2011-07-05
|
\
|
*
1. generating a separate dipatchcontinuation label for each trycatchfinally ...
qadeer
2011-07-04
*
|
Merge
Mike Barnett
2011-06-29
|
\
|
[next]