| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
type exist. This remains a work in progress
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
| |
for BvExtractExpr, BvConcatExpr and OldExpr.
|
| |
|
|
| |
for LiteralExpr, IdentifierExpr and NAryExpr.
|
| |
|
|
| |
are immutable. Add unit tests to check this.
|
| |
|
|
| |
to set them as immutable (not currently enforced for these Expr types).
|
| |
|
|
|
| |
Add a unit test for this. We need to protect the Args field too
but that is going to be much harder to enforce.
|
| |
|
|
| |
to check this is being enforced.
|
|
|
For IdentifierExpr and the Type field of Expr.
There are lots of places where it still isn't enforced but hopefully
we'll fix those in due time.
|
Dietrich
Dan Liew