| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
mantissa and exponent
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Made changing the reference throw an exception if the NAryExpr was
constructed as immutable
* Changed the type of NAryExpr.Args to be IList<Expr> rather than
List<Expr> so that when the NAryExpr is immutable I can return
``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read
only wrapper around the List<Expr> so that clients cannot change the
list.
I came across two problems
* Making this change required changing types all over the place (from
List<Expr> to IList<Expr>). I feel that changes are extensive enough
that there's a good chance that out of tree clients using Boogie's
libraries might break. I've waited for a code review but this didn't
happen so I'm committing anyway.
* I came across something that looks like bad design of the IAppliable
interface which potentially breaks immutability enforcement. I've left
this as a "FIXME" in this. Here's the problematic method.
```
Type Typecheck(ref List<Expr>/*!*/ args, out
TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/
tc);
```
It potentially allows the instance of the args to be changed which
seems very suspect.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
- making field private
- adding getter/setter
- copying incoming list
- exposing read-only list
(with help from David Rohr)
|
| | |
| |
| |
| |
| |
| |
| |
| | |
- making field private
- exposing read-only list
- copying incoming list
- adding methods 'AddParam', 'AddParams', and 'ClearParams'
(with help from David Rohr)
|
| |/
|
|
|
|
| |
-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)
|
| | |
|
| |
|
|
| |
Added an internal non-readonly version of Lhss and Rhss to 'AssignCmd'.
|
| | |
|
| |
|
|
|
|
| |
before real verification.
Fixed treatment of lambda-expression attributes.
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
| |
made the default phase of assertions be 0
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
interval-based abstract interpretation instead.
Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie.
Command-line option '/logInfer' has been dropped.
|
| | |
|
| | |
|
| |
|
Checkmate50
wuestholz
Dan Liew
Unknown
qadeer