| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
enabled it to be always on
|
| |
|
|
| |
many of the test suite dirs
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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 %
|
| |
|
|
| |
parameters
|
| |
|
|
| |
define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations.
|
| |
|
|
| |
label in the current implementation.
|
| |
|
|
|
|
|
|
|
| |
* Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners.
* It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs.
Dafny:
* Ditto for its Parser.cs/Scanner.cs.
* Added ability to provide a custom Errors handler for scanner/parser.
* Added Test/dafny1/Cubes.dfy
|
| |
|
|
|
|
| |
having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories.
Lots of code changes to compensate for the new frame files.
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
are run.
|
| |
|
qadeer
Pantazis Deligiannis
Unknown
Unknown
Rustan Leino
qadeer