| Commit message (Collapse) | Author | Age |
|
|
|
| |
namespaces remain the same.
|
|
|
|
| |
directly included in ProverInterface.cs.
|
|
|
|
| |
Codeplex repositories.
|
|
|
|
| |
Codeplex repositories.
|
|
|
|
| |
on Codeplex
|
| |
|
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
Dafny: included FloydCycleDetect again (which had been temporarily commented out)
DafnyExtension: adjusted to Boogie's change in abstract-interpretation support
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
|
|/
|
|
| |
of / and %
|
|
|
|
| |
and axiomatize [][..0] == [] == [][0..]
|
| |
|
|
|
|
| |
parallel statements.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
into Boogie
Dafny: started cloning of refined classes
Dafny: added /rprint switch to print the (syntax of the) resolved Dafny program
|
|
|
|
| |
method as a good candidate for inlining (supported in .NET 4.5)
|
|
|
|
| |
not with a substitution)
|
|
|
|
| |
axioms that use it
|
|
|
|
| |
assignment statement where the LHS has the form a[lo..hi])
|
|
|
|
| |
Dafny: beefed up resolution of parallel statements
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
with duplicate array.Length functions in generated Boogie file.
|
| |
|
| |
|
|
|
|
| |
runtime.)
|
| |
|
| |
|
| |
|
|
|
|
| |
added function $IsCanonicalBoolBox
|
|
|
|
| |
avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
|
| |
|
| |
|
|
|
|
|
|
| |
Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction
Dafny: split expressions when proving function postconditions
Boogie and BVD: updated copyright year ranges
|
|
|
|
| |
Ignore duplicated else functions in models
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case).
* Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.)
* Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type.
* More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal")
* Add axioms about idempotence of set union and intersection
* The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one
* In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase
* Fixed error in translation of while(*)
|
|
|
|
|
| |
Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT.
Add default Z3 options when using Z3.
|