index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
BCT
/
RegressionTests
Commit message (
Expand
)
Author
Age
*
Fixed two bugs related to structs: now a struct that is declared without an
Mike Barnett
2011-09-01
*
Made the split fields heap agree with the naming convention used for fields that
Mike Barnett
2011-08-16
*
Fixed problem where events in stubs were generating duplicate declarations.
Mike Barnett
2011-08-11
*
(BCT) BREAKING CHANGE
t-espave
2011-08-11
*
(phone bct) nav graph building (mostly) automated
t-espave
2011-08-05
*
Added new option /captureState (/c) for generating a capture state assumption
Mike Barnett
2011-08-04
*
Changed name mangling (again) to avoid name clashes.
Mike Barnett
2011-08-04
*
Increase the name mangling to avoid name clashes in the Boogie program. In IL,
Mike Barnett
2011-08-03
*
(phone bct) default URI checks inlined
t-espave
2011-08-02
*
Fix in the assertion injector for putting the output on top of the input
Mike Barnett
2011-08-01
*
Merge
Mike Barnett
2011-07-27
|
\
*
|
Implemented a whitelist/blacklist so translator can ignore certain parts of an
Mike Barnett
2011-07-27
|
*
fixed right/left shift functions decl
t-espave
2011-07-27
|
/
*
Updated regressions.
Mike Barnett
2011-07-27
*
adding checks and code injection for phone feedback checking
t-espave
2011-07-25
*
Added subtyping axiomatization.
Mike Barnett
2011-07-20
*
Add a translation for switch statements.
Mike Barnett
2011-07-14
*
phone control exploration for BCT, not integrated yet
Unknown
2011-07-07
*
Updated regression output.
Mike Barnett
2011-07-06
*
Updated regression output.
Mike Barnett
2011-07-06
*
Fixed/improved the handling of conditional expressions.
Mike Barnett
2011-05-31
*
Added bitwise operations.
Mike Barnett
2011-05-31
*
Lots of small bug fixes: conversions, overloaded operations on real numbers.
Mike Barnett
2011-05-31
*
Handle more conversions.
Mike Barnett
2011-05-29
*
Fixes for a bunch of different bugs. Translate default value for doubles,
Mike Barnett
2011-05-29
*
Removed the method DefaultValue from the sink: if a default value of a type
Mike Barnett
2011-05-29
*
Translate assignments to parameters that are of a struct type correctly. Note
Mike Barnett
2011-05-28
*
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
*
Created an API so that a MetadataTraverser is used to translate a set of
Mike Barnett
2011-05-21
*
Unify translation of arguments so the same code is used for IMethodCall and
Mike Barnett
2011-05-19
*
Add extern declarations to procedures.
Mike Barnett
2011-05-16
*
Trying to fix the bound expression simplifier.
Mike Barnett
2011-05-12
*
Cleanup of new LHS simplification and replaced the golden output with the
Mike Barnett
2011-05-06
*
The decompilation is not guaranteed to get rid of all push statements and pop
Mike Barnett
2011-04-29
*
Model newly constructed structs as a constant DefaultStruct that has axioms that
Unknown
2011-04-27
*
merge changes with shaz's checkin.
Unknown
2011-04-27
|
\
|
*
Trying to get structs supported.
Unknown
2011-04-27
*
|
fixes to struct translation
qadeer
2011-04-27
|
/
*
0. Deleted other heap representations except SplitField and General
qadeer
2011-04-23
*
Fix stub support (still not completely finished).
Unknown
2011-04-12
*
More support for stubs. Ability to add functions as well as procedures.
mikebarnett
2011-04-04
*
Can now translate multiple assemblies into one Boogie Program.
mikebarnett
2011-03-08
*
Made it unnecessary to set the types on the Boogie ASTs as we create them.
mikebarnett
2011-03-03
*
Create a static constructor only for types that don't already define one.
mikebarnett
2011-03-02
*
Fixed many bugs.
mikebarnett
2011-03-01
*
implemented delegates and events
qadeer
2011-02-25
*
Added a new type, Type, that represents runtime types. The Heap interface now...
mikebarnett
2011-02-24
*
Changed calls to Debug.Assert to Contract.Assert.
mikebarnett
2011-02-24
*
Fix the generation of procedure names so that array types are encoded properly.
mikebarnett
2011-01-26
[next]