| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
LiteralExpr to Expr. Enforcing the return type be LiteralExpr is
too restrictive.
There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.
Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.
a visitor that does constant folding of an Expr tree
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
ExistsExpr to Expr. Enforcing the return type be ExistsExpr is
too restrictive. For example it prevents anyone from implementing
a visitor that does constant folding of an Expr tree.
There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.
Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.
a visitor that does constant folding of an Expr tree
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
ForAllExpr to Expr. Enforcing the return type be ForAllExpr is
too restrictive. For example it prevents anyone from implementing
a visitor that does constant folding of an Expr tree.
There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.
Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.
a visitor that does constant folding of an Expr tree
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr is
too restrictive. For example it prevents anyone from implementing
a visitor that does constant folding of an Expr tree.
There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.
Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.
a visitor that does constant folding of an Expr tree
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is
too restrictive. For example it prevents anyone from implementing
a visitor that does constant folding of an Expr tree.
There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.
Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.
|
| |
|
|
|
|
| |
-replacing public field by private field + getter
-using read-only wrappers (to avoid leaking)
-cloning the tr list in the setter and constructor (to avoid capturing)
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
There were many calls in the code to
``` new TokenTextWriter("<buffer>", buffer, false) ```
Prior to 61a94f409975 this was a call to the following constructor
```
TokenTextWriter(string filename, TextWriter writer, bool setTokens)
```
After that commit these then became calls to
```
TokenTextWriter(string filename, TextWriter writer, bool pretty)
```
An example of where this would cause issues was if ToString() was called on an
AbsyCmd then the its token would be modified because the setTokens parameter
was effectively set to True when the original intention was for it to be set
to false!
To fix this I've
* Removed the default parameter value for pretty and fixed all
uses so that we pass false where it was implicitly being set before
* Where the intention was to set setTokens to false this has been fixed so
it is actually set to false!
Unfortunately I couldn't find a way of observing this bug from the Boogie
executable so I couldn't create a test case. I could only observe it when I was
using Boogie's APIs.
|
| |
|
|
|
|
| |
of its methods now demand the return value to equal the given node.
Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
now positive/negative context is detected and appropriate translation is done
|
| |
|
|
| |
alternative existential semantics.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
code (as opposed to contracts).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | |\
| |/
|/| |
|
| | | |
|
| | | |
|
| |/| |
|
| | | |
|
| | | |
|
| | | |
|
| | |\
| |/
|/| |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
| |
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)
|
Valentin Wüstholz
wuestholz
Dan Liew
Pantazis Deligiannis
Unknown
Unknown