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
*
phone methods boogie stubs
Unknown
2011-07-12
*
injecting code for phone control initialization during translation
Unknown
2011-07-12
*
- removed "exit 43" from StartDafny-jen.bat
Unknown
2011-07-12
*
Merge
Rustan Leino
2011-07-11
|
\
*
|
Dafny: allow constructors only inside classes, removed semi-colons at end of ...
Rustan Leino
2011-07-11
|
*
- added the "timeout" option
Unknown
2011-07-11
|
*
- typos
Unknown
2011-07-11
|
*
- fixed a bug in DafnyModelUtils.fs (reading set values from models)
Unknown
2011-07-11
|
*
Merge
Unknown
2011-07-11
|
|
\
|
|
*
- added Set.jen example
Unknown
2011-07-11
|
*
|
async call return value is either int or bv32
qadeer
2011-07-09
|
*
|
added a new regression
qadeer
2011-07-09
|
*
|
Merge
qadeer
2011-07-09
|
|
\
\
|
*
|
|
fixed bug in vcgen for bitvectors
qadeer
2011-07-09
|
|
|
*
- removed VarConst from Const
Unknown
2011-07-08
|
|
*
|
phone injecting code traverser
Unknown
2011-07-08
|
|
*
|
Dafny: Added Euclidean regression test (Verifier only).
Jason Koenig
2011-07-08
|
|
*
|
Merge
Jason Koenig
2011-07-08
|
|
|
\
\
|
|
|
/
/
|
|
/
|
|
|
|
*
|
Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run...
Jason Koenig
2011-07-08
|
*
|
|
Merge
Mike Barnett
2011-07-08
|
|
\
\
\
|
*
|
|
|
Fix translation of "is" operator.
Mike Barnett
2011-07-08
|
|
*
|
|
phone stuff options
Unknown
2011-07-08
|
|
|
/
/
|
|
*
/
phone control exploration for BCT, not integrated yet
Unknown
2011-07-07
|
|
/
/
|
*
|
Chalice: Fix workitem 10191 (escaping method arguments).
stefanheule
2011-07-07
|
*
|
Chalice: New test script to execute all tests (in all folder) at once. Test s...
stefanheule
2011-07-07
|
*
|
Chalice: Error message of the valid-permission-check often included '<undefin...
stefanheule
2011-07-07
|
*
|
Chalice: Allow _ as wildcard in the eval construct for parameters. Usage is d...
stefanheule
2011-07-07
|
|
/
|
*
- fixed some bugs with applying unification over list elements
Unknown
2011-07-06
|
*
Merge
Unknown
2011-07-06
|
|
\
|
*
|
remove mscorlib stub project...write each as needed
Unknown
2011-07-06
|
|
*
Merge
Mike Barnett
2011-07-06
|
|
|
\
|
|
|
/
|
|
/
|
|
|
*
Updated regression output.
Mike Barnett
2011-07-06
|
*
|
phone (static) controls extractor
Unknown
2011-07-06
|
*
|
phone (static) controls extractor.
Unknown
2011-07-06
|
/
/
*
|
Merge
Jason Koenig
2011-07-06
|
\
\
*
|
|
Dafny: Fixed bug in call statements where mutability of out parameters was no...
Jason Koenig
2011-07-06
|
*
|
Merge
Unknown
2011-07-06
|
|
\
\
|
|
/
/
|
/
|
|
|
*
|
- implemented some sorts of symbolic evaluation of expressions
Unknown
2011-07-06
|
|
*
Merge
Mike Barnett
2011-07-06
|
|
|
\
|
|
_
|
/
|
/
|
|
|
|
*
Beginning of encoding the subtype relation.
Mike Barnett
2011-07-06
|
|
*
Updated regression output.
Mike Barnett
2011-07-06
*
|
|
Chalice: fix workitem 10194 (unfolding and old-expressions).
stefanheule
2011-07-06
*
|
|
Chalice: fix workitem 10199 (partial unfolding of nested predicates).
stefanheule
2011-07-06
|
*
|
- implemented synthesis of some simple constructors with parameters
Unknown
2011-07-05
*
|
|
Merge
Jason Koenig
2011-07-05
|
\
\
\
*
|
|
|
Dafny: Updated regression tests to include chaining disjoint operators.
Jason Koenig
2011-07-05
*
|
|
|
Dafny: Added chaining of disjoint (!!) using transitive chaining convention.
Jason Koenig
2011-07-05
|
*
|
|
ExtractLoops calls the same code for eliminating unreachable blocks that norm...
qadeer
2011-07-05
|
*
|
|
Don't send (check-sat) after error limit is reached
Michal Moskal
2011-07-05
|
*
|
|
Merge
Michal Moskal
2011-07-05
|
|
\
\
\
|
|
/
/
/
|
/
|
|
|
[next]