| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
/proverWarning switch).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior
* Made Dafny check loops for termination by default. Previously, this was done only if the loop had a decreases clause. To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *".
* Allow "reads *" to say that the function may read anything at all (sound, but not very useful)
* Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated
* Added some previously omitted well-definedness checks.
* Fixed some bugs in the resolver that caused some type errors not to be reported
* Added some messages to go with some (previously rather opaquely reported) errors
* Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted)
* Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked. The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.
|
| |
|
|
|
|
| |
bodies) match expressions.
Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
StandardVisitor while visiting commands).
This solves Issue #6266.
|
| | |
|
| |
|
|
| |
statements and writes them the stdout. Line numbers are only displayed for bpl input.
|
| |
|
|
| |
Included VSI-Benchmarks in standard tests.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
and seq.
Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).
Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.
Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.
Added a space in the pretty printing of Boogie coercion expressions.
|
| |
|
|
| |
variables, if they were not already local variables.
|
| |
|
|
|
|
|
| |
"!(x in S)".
Changed Dafny test files to use the new operator.
Included the file b8.dfy into the VSI-Benchmarks test harness.
|
| | |
|
| |
|
|
|
|
| |
added first test cases for doomed (including the ones from smoke)
minor bug fixes
minor speed-ups
|
| | |
|
| | |
|
| |
|
|
|
|
| |
caused malformed Boogie and malformed VCs. In particular, the problem arose in the CEV $file_name_is declarations. Such characters are now replaced by a percent sign followed by a four-digit hexadecimal number representing the Unicode value of the character.
This fixes issue #6057.
|
| |
|
|
|
|
| |
is being executed from, then look in "c:\Program Files\Microsoft Research\Z3-2.x\bin" for x := 5,4,3,2,1,0.
This fixes Issue Tracker item 5446.
|
| |
|
|
|
|
| |
filename starts with a digit, don't just prepend it to a QID, but prepend another character ('_') first.
This fixes issue 5278 in the Issue Tracker.
|
| |
|
|
| |
This solves issue 5742, as reported in the MSR Boogie Issue Tracker on Codeplex.
|
| |
|
|
| |
quantifier. This makes sure that we get the proper DEFTYPEs for bit vector variables, even when they are not used in operator expressions. Fixes issue #5741.
|
| |
|
|
| |
to Z3. By default, both LET TERM and LET FORMULA expressions are used. Mode /z3lets:2 uses only LET FORMULA, which works around a current Z3 issue with LET expressions and nested quantifiers.
|
| | |
|
| |
|
|
| |
Deleted/ignored some binaries in the Binaries directory.
|
| |
|
|
| |
antecedent in select-of-store axioms (fixing an error in my previous check-in).
|
| | |
|
| |
|
|
| |
triggers are ignored.
|
| |
|
|
| |
assert (switches off z3's /@ flag).
|
| |
|
|
|
| |
* SscBoogie: changed default setting for /modifiesOnLoop
(we really should move this SscBoogie-specific code to the Spec# codeplex)
|
| |
|
|
|
| |
Dafny: Make use of function preconditions in function well-definedness checks.
Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
|
| |
|
|
|
|
|
|
| |
* Added DeclType(f)==C axioms, which for each field f says which class declares it.
Boogie:
* Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
|
| | |
|
| |
|
|
| |
stdout/stderr
|
| |
|
|
| |
bitvector operations
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Boogie.
|
| |
|
|
| |
start block. Now it does. After the remove-empty-blocks optimization, the only possibly empty block is the start block. That is, the optimization does not change the name of the start block.
|
| |
|
|
| |
and not just the LKG.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
mkawa