| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
The functionality is currently broken.
* Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it)
* Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
|
| |
|
|
|
|
|
| |
linear procedure call
2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation. These are set just before inlining is called and now I reset them to null afterwards to help garbage collection.
3. Clear live variables right after passification again to help garbage collection.
|
| |
|
|
| |
Controlled by the option /coalesceBlocks (default is to perform the optimization).
|
| |
|
|
| |
generation. This reduces the chances of Boogie causing a stack overflow.
|
| |
|
|
|
|
| |
* Allow ghost methods (all "ghost" keywords are currently parsed and then ignored)
* Improved and made more automatic the treatment of "use" functions (a good next step would be to automatically infer which functions would make good "use" functions)
* Include preconditions in all definedness checks of function-call expressions
|
| | |
|
| |
|
|
|
|
| |
2. Hoisted the call to inlining into BoogieDriver.ssc
3. Implemented a simple dead variable elimination
4. Perform inlining only for those procedures whose verification is not skipped
|
| | |
|
| | |
|
| |
|
|
| |
information
|
| |
|
|
| |
by explorer
|
| | |
|
| |
|
|
|
|
|
|
| |
boolean-only if-then-else expressions)
Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Test/doomed/doomdebug.bpl
|
| |
|
|
| |
result types of maps are declared before the type of the map itself.
|
| |
|
|
| |
used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.
|
| |
|
|
|
|
|
| |
* Allow (and currently ignore) "ghost" modifier.
* Fixed bug in boxing.
* Check for div-by-zero error for modulo operator.
* Improved emacs and latex modes.
|
| |
|
|
| |
theorem prover calls (See useCE in notdoomed.bpl).
|
| |
|
|
|
|
|
|
| |
pretty-printer use ":" not "returns".
Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions.
Consequently foo(int,y:bool) is no longer allowed.
Update the testsuite to match that.
|
| | |
|
| | |
|
| |
|
|
|
| |
print _all_ the attributes of an assert this time
add simpletypes to the visitor
|
| | |
|
| |
|
|
| |
/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.
|
rustanleino