| 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.
|
| |
|
|
|
|
| |
is not correctly set. This is related to the bug fixed in cea703affa29. That
commit fixed the ShallowType when it was set using the constructor that takes
a Function but the parser uses the other constructor which has the same bug.
|
| |
|
|
| |
fails when the Function is a FunctionCall
|
| |
|
|
|
|
|
| |
added unit tests csproj files from 12.0 to 4.0. This done so that Monodevelop
5.0.1 can import these projects (it can't handle the newer ToolsVersion).
This didn't seem to break anything in Visual Studio 2013
|
|
|
so developers need to install it via NuGet.
There aren't many tests yet. Just a few for Core and Basetypes but
hopefully more will be added in the future.
More information can be found in Source/UnitTests/README.md
|
Checkmate50
Dan Liew