| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
conversion from Spec# into C# moved a constructor call
|
|
|
|
|
|
|
|
|
| |
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)
|
| |
|
| |
|
|
|
|
|
|
| |
dictionaries are non-null, which is enforced by the implementation of Dictionary.
Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
|
|
|
|
| |
And/Or nodes.
|
|
|
|
|
|
| |
* enhanced the printing of captured states
* addressed some warnings issued by VS 2010
* some code formatting
|
|
|
|
| |
fewer error messages when compiling with runtime checking on.
|
| |
|
| |
|
| |
|
|
|