| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
floating points could not be given as a function argument
|
| |
|
| |
|
|
|
|
| |
to 97/98 (from 135/136)
|
| |
|
|
|
|
| |
in a future commit
|
| |
|
| |
|
|
|
|
| |
public field by private field + getter/setter).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
and Parser constructors have been modified to take an optional
argument specifying this and the ExecutionEngine passes for that
value CommandLineOptions.Clo.UseBaseNameForFileName
This option when true causes the basename of file to be used inside
created Tokens instead of what the user passed on the command line
which might be a relative or absolute path.
The motivation for adding this option is that it is needed for the
lit driven tests so that the output of Boogie can be reliably checked.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
fixed BCT :value
|
|
|
|
| |
some trailing whitespace.
|
|
|
|
|
|
| |
files generated by Coco/R.
This was done to support sharing of the Coco/R .frame files with Spec#.
|
|
|
|
|
|
|
|
|
| |
* 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
|
| |
|
|
|