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
*
Changes needed to translate both contracts and method bodies. The Statement a...
mikebarnett
2011-03-05
*
Dafny: Added heuristic for when to turn on the induction tactic
rustanleino
2011-03-05
*
changes for dealing with delegates
qadeer
2011-03-05
*
Dafny:
rustanleino
2011-03-04
*
Fix translation of "new" so that a procedure is generated (if needed) for the...
mikebarnett
2011-03-03
*
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
*
put the call to CreateStaticConstructor back in
qadeer
2011-03-02
*
some fixes
qadeer
2011-03-02
*
Fix null-equivalent initialization of fields so that instance fields are init...
mikebarnett
2011-03-02
*
fixes for splitFields option
qadeer
2011-03-02
*
Use the Sink's API for creating a procedure for the Invoke method of a delegate.
mikebarnett
2011-03-01
*
Fixed many bugs.
mikebarnett
2011-03-01
*
Boogie build succeeded, 4 test(s) failed
codeplexbot
2011-03-01
*
Dafny: support for nested match expressions
rustanleino
2011-03-01
*
Updates to Answer files from recent changes
rustanleino
2011-03-01
*
Boogie build succeeded, 5 test(s) failed
codeplexbot
2011-02-27
*
Dafny: Non-empty Visual-Studio error messages for related split-expr locations.
rustanleino
2011-02-27
*
Fixed dynamic dispatch so the most derived override is called for each subtype.
mikebarnett
2011-02-25
*
two bug fixes
qadeer
2011-02-25
*
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
*
Boogie build succeeded, 4 test(s) failed
codeplexbot
2011-02-24
*
Changed calls to Debug.Assert to Contract.Assert.
mikebarnett
2011-02-24
*
Mimic Z3 logic for figuring out the blocking clause for the next counterexample
MichalMoskal
2011-02-23
*
Don't ever put a label under a quantifier.
MichalMoskal
2011-02-23
*
Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)
MichalMoskal
2011-02-23
*
Add IEnumerable.Concat1 method.
MichalMoskal
2011-02-23
*
Add tests for -z3multipleErrors from Shuvendu.
MichalMoskal
2011-02-23
*
Fix build by adding missing project.
mikebarnett
2011-02-23
*
Boogie build succeeded, 4 test(s) failed
codeplexbot
2011-02-23
*
Boogie build succeeded, 26 test(s) failed
codeplexbot
2011-02-23
*
Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly different...
MichalMoskal
2011-02-23
*
Check for timeout/memoryout
MichalMoskal
2011-02-23
*
Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing...
MichalMoskal
2011-02-23
*
Don't try to declare bv types
MichalMoskal
2011-02-23
*
Dispose of the prover when Close() is called.
MichalMoskal
2011-02-23
*
Add workaround for cmd race
MichalMoskal
2011-02-23
*
Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!)
MichalMoskal
2011-02-23
*
Pass solverarguments
MichalMoskal
2011-02-23
*
Do typed->untyped translation for -mv variables
MichalMoskal
2011-02-23
*
Provide dummy implementation of FlushAxiomsToTheoremProver()
MichalMoskal
2011-02-23
*
Handle as-array[...] model elements
MichalMoskal
2011-02-23
*
Fixes in /useArrayTheory handling
MichalMoskal
2011-02-23
*
Parse else-> clauses in the model
MichalMoskal
2011-02-23
*
Throw exceptions when push/pop interface is used but not implemented
MichalMoskal
2011-02-23
*
Pass :skolemid to SMTLib prover
MichalMoskal
2011-02-23
*
Implement Push/Pop interface.
MichalMoskal
2011-02-23
*
Allow recent Z3 versions to be used
MichalMoskal
2011-02-21
*
Move model printing to ErrorModel class
MichalMoskal
2011-02-21
[next]