index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
BCT
Commit message (
Expand
)
Author
Age
*
Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codepl...
Rustan Leino
2013-03-05
*
Find implementations of interface methods for dynamic dispatch, not just
Unknown
2012-09-09
*
Avoid creating a dynamic dispatch table for GetHashCode and ToString: it ends
Unknown
2012-09-09
*
Moved the statement traverser's operand stack (used for explicit push/pop/dup
Unknown
2012-09-09
*
Fix the whole-program translator so that exception handling is done
Unknown
2012-08-23
*
Make the modelExceptions option an integer.
Unknown
2012-08-22
*
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
*
When translating an assighment, leave the source of the assignment on the
Unknown
2012-06-02
*
Don't add dummy modules (resulting from a failed load) to the list of modules
Unknown
2012-06-02
*
Fix for addressof expressions.
Unknown
2012-05-18
*
Add options to control the emission of free ensures for
Unknown
2012-04-16
*
Removed expression simplifier (actually just commented
Unknown
2012-04-15
*
Added "free ensures" to procedures encoding the allocatedness
Unknown
2012-04-10
*
Fix a lot of the translation of "op=" expressions
Unknown
2012-04-09
*
Changed the BCT solution so it uses the CodePlex version of CCI (instead
Mike Barnett
2012-03-30
*
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
|
*
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
|
*
Automated merge with https://hg01.codeplex.com/boogie
Mike Barnett
2012-02-27
|
/
|
|
*
Adapting to new decompiler.
Mike Barnett
2012-02-27
*
|
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
|
/
*
Union is now based on axioms
qadeer
2012-02-07
*
fixed bug in model parsing
qadeer
2012-02-06
*
Merge
qadeer
2012-02-06
|
\
*
|
added inlining support for all implementations given the attribute {:inline 1}
qadeer
2012-02-06
|
*
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 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
*
|
|
added another method that just throws an exception
qadeer
2012-01-24
|
/
/
*
/
an optimization in dynamic dispatch
qadeer
2012-01-23
|
/
*
Mark the procedure translated from the module's entry point
Mike Barnett
2012-01-15
*
Make a copy of a struct value being passed to a method
Mike Barnett
2012-01-10
*
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
*
Copy structs that are passed by value as method call arguments.
Mike Barnett
2012-01-04
*
For now, just ignore "address of" nodes and translate the expression of which
Mike Barnett
2012-01-03
*
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
*
problem fixed after CCI update
qadeer
2011-12-30
[next]