index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Merge
t-espave
2011-07-26
|
\
|
*
added translation for RightShift and LeftShift
Unknown
2011-07-26
*
|
bugfix on null assignments
t-espave
2011-07-26
*
|
tracking new controls
t-espave
2011-07-26
*
|
ignoring (some) non-feedback producing event handlers
t-espave
2011-07-26
|
/
*
Merge
t-espave
2011-07-26
|
\
*
|
weeding out non-set $exception as feedback handling issues
t-espave
2011-07-26
|
*
Merge
Rustan Leino
2011-07-26
|
|
\
*
|
|
ui handlers override checked for output geenration
t-espave
2011-07-26
|
|
*
- restored the "old" (as it was before switching from map to list)
Unknown
2011-07-25
|
|
*
- changed heapInst.assignments' type from Map to List (because assignment or...
Unknown
2011-07-25
*
|
|
Merge
t-espave
2011-07-25
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
adding checks and code injection for phone feedback checking
t-espave
2011-07-25
|
|
*
Merge
Rustan Leino
2011-07-25
|
|
|
\
|
|
|
/
|
|
/
|
|
*
|
Merge
Unknown
2011-07-22
|
|
\
\
|
|
/
/
|
/
|
|
*
|
|
tracking main phone application class and ctors
t-espave
2011-07-22
*
|
|
typo
t-espave
2011-07-22
*
|
|
double definition fix
t-espave
2011-07-22
*
|
|
Chalice: Check definedness of where-clause of channels (was missing before), ...
stefanheule
2011-07-22
*
|
|
Chalice: Improve smoke testing: look for preconditions of functions, predicat...
stefanheule
2011-07-22
|
*
|
Jennisys: added Jennesys/Jennesys/examples/bak to hgignore
Unknown
2011-07-21
|
*
|
Jennisys:
Unknown
2011-07-21
|
|
*
Merge
Rustan Leino
2011-07-21
|
|
|
\
|
|
*
|
Dafny: call previous lemma instead of restating it
Rustan Leino
2011-07-21
*
|
|
|
cleanup
t-espave
2011-07-21
|
|
_
|
/
|
/
|
|
*
|
|
Merge
t-espave
2011-07-21
|
\
\
\
*
|
|
|
dynamic navigation variable tracking and base page name tracking
Unknown
2011-07-21
|
*
|
|
Chalice: Only show the "first" smoke warning, as once the prover is able to s...
stefanheule
2011-07-21
*
|
|
|
unified URI format across translations
Unknown
2011-07-21
|
/
/
/
*
|
|
setting $Exception explicitly to null in phone translation
Unknown
2011-07-20
*
|
|
fixed a bug on current nav tracking
Unknown
2011-07-20
*
|
|
Merge
Jason Koenig
2011-07-20
|
\
|
|
*
|
|
Merge
Jason Koenig
2011-07-20
|
\
\
\
|
|
*
\
Merge
Unknown
2011-07-20
|
|
|
\
\
|
|
*
|
|
- changed the way Valid() is unrolled
Unknown
2011-07-20
|
|
|
*
|
updated translation of catch clauses to use Subtype
qadeer
2011-07-20
|
|
|
/
/
|
|
*
|
Added subtyping axiomatization.
Mike Barnett
2011-07-20
|
|
*
|
Chalice: Use "/smoke" for the test suite by default to ensure test quality. U...
stefanheule
2011-07-20
|
|
*
|
Chalice: improve smoke testing to use the subsumption option only for the "as...
stefanheule
2011-07-20
|
|
*
|
Chalice: Improve command line help and allow both "-param" (old) and "/param"...
stefanheule
2011-07-20
|
|
*
|
Chalice: Uniform usage of Boogie syntax for functions.
stefanheule
2011-07-20
|
|
*
|
Merge
Unknown
2011-07-19
|
|
|
\
\
|
|
|
*
|
- added synthesized code for the examples
Unknown
2011-07-19
|
|
|
*
|
- added synthesis of Repr stuff (it generates Repr invariants,
Unknown
2011-07-19
|
|
*
|
|
edited out phoneplugin from most places
Unknown
2011-07-19
|
|
/
/
/
*
|
|
|
Fixed axiom for Take/Update commuting.
Jason Koenig
2011-07-19
|
*
|
|
Chalice: Fix all three copyless message passing programs. There were problems...
stefanheule
2011-07-19
|
*
|
|
Chalice: Fix two nasty bugs that could lead to contradictions in the Boogie e...
stefanheule
2011-07-19
|
*
|
|
Chalice: Fix batch file problem and update reference output.
stefanheule
2011-07-19
|
*
|
|
boogie boilerplate code generator for phone verif.
Unknown
2011-07-18
[next]