| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
|
| | |
|
| |
|
|
| |
affect preconditions.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
anything that implements the IAppliable interface. Type checking
should never need to change the reference of a list of arguments
(hence the removal of the ``ref`` keyword) and we need to use IList<Expr>
instead of List<Expr> to allow NAryExpr to do its type checking.
|
| |
|
|
| |
even if the types are equivalent.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
|
|
| |
If constructing immutable Expr bottom up this would be very inefficient
because the hashcode would be recomputed unnecessarily. Now just make
ComputeHashCode() methods call GetHashCode() on Expr instead.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
<bool> == <bool>
or
<bool> != <bool>
The type checker tries rewrite the Expr when it gets type checked
which breaks immutability so disable doing this if the Expr is
immutable.
|
| |
|
|
| |
assumption variables.
|
| |
|
|
|
| |
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.
|
| |
|
|
|
|
| |
has never been type checked we allow the Type field to be set but
once it has been set it cannot be changed to refer to a different
Type.
|
| |
|
|
|
| |
immutable by raising an exception if an attempt is made to modify it
after construction.
|
| |
|
|
|
|
|
| |
for doing this is that we would like a LiteralExpr to be immutable
when constructed but because the "Val" field can point to a BvConst
which is an object it means that although the Val reference cannot
change the BvConst could be changed.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This is currently not enforced (it really should be). So right now it
only amounts to a promise by the client that the Expr will not be modified
after it is constructed. We should actually enforce this by protecting
various fields of the Expr classes so they can't be changed if an Expr
is constructed as Immutable.
The motivation for doing this is it allows the value of GetHashCode()
to be cached. Expr classes now implement ComputeHashCode() to do the
actuall hash code computation.
|
| | |
|
| |
|
|
| |
(replaced public field by private field + getter/setter)
|
| | |
|
| | |
|
| |
|
|
|
|
| |
becomes availble via ShallowType().
This fixes the ExprTypeChecking.FunctionCallTypeResolved() unit test.
|
| |
|
|
|
|
|
|
|
| |
unit test to fail.
The issue was that one of FunctionCall constructors created a new IdentifierExpr
without associating a type with it. To fix this we now set the type of
the IdentifierExpr to the return type of the Function passed into the
constructor.
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
true but A.GetHashCode() == B.GetHashCode() return false.
The case of the bug was that Args.GetHashCode() was being used which
uses Object.GetHashCode() which uses references to compute GetHashCode().
This is wrong because we want hash codes to equal for structural equality.
To fix this I've implemented a really simple hashing method. I have not tested
how resilient this is to collisions.
|
| |/
|
|
|
|
|
|
| |
The previous implementation which called object.Equals(this.Args, other.Args)
would in turn call ``this.Args.Equals(others.Args)`` which for List<> is
reference equality. Equals() is purposely overloaded on Expr classes in Boogie
to provide structural equality so this has been fixed so a comparision of
elements in the list is performed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
advanced verification result caching even for implementations with errors.
|
| |
|
|
|
|
| |
When running boogie form the command line, this should be on by default.
On the other hand, the TokenTextWriter constructors and PrintBplFile now have an
argument for this, but by default it is off.
|
| |
|
|
| |
others already present for bool, BigNum and BigDec.
|
| |
|
|
|
| |
Reduce depth of AST whenever possible (e.g., use a binary tree instead of a
linear list of terms)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Checkmate50
Dan Liew
Valentin Wüstholz
wuestholz
Dan Rosén
Unknown