| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
Cmd classes but for some reason it wasn't implemented for TransferCmds
which seems a little inconsistent.
|
| |
|
|
|
| |
Previously after duplication of an entire program CallCmd.Proc would
point to procedures in the old program.
|
| |
|
|
|
|
| |
Absy metadata. This feature is very new so it is unlikely any out
of tree code (apart from my own) is using it so this change shouldn't
be disruptive.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
a cloned Implementation.Proc would not be the same Procedure in
the TopLevelDeclarations.
The reason for this is that Procedure would be cloned twice, once
when visiting it from the TopLevelDeclarations and once when visiting
each Implementation of that Procedure's Implementation.Proc.
To fix this a Procedure is only duplicated once by caching it based
on reference value (this assumes the original Program has Procedure
and Implementation.Proc correctly resolved). This also assumes that
Procedure.Equals() and Procedure.GetHashCode() have not been overidden.
|
| |
|
|
|
| |
Instead of the Duplicator maintaining state the VisitImplementation()
method computes the mapping between old and new Blocks.
|
| |
|
|
|
|
|
|
|
|
|
| |
where not updated during duplication to point to duplicated BasicBlocks.
Because the lists weren't being duplicated and resolved to the new basic blocks
a duplicated Implementation pointed into Blocks in the old implementation via
GotoCmds. This is bad and is not the expected behaviour.
Now if VisitImplementation() is called during duplication GotoCmds will be
resolved to point to duplicated Blocks.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
condition is assumed while inlining.
|
| | |
|
| | |
|
| |
|
|
| |
changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
integer as a key. This allows any arbitrary "metadata" to be attached
at runtime. The implementation is lazy so the container is only created
if the SetMetadata<T>() method is called which should keep the memory
overhead very minimal.
Example usage:
var TheAssert = new AssertCmd(...);
...
TheAssert.SetMetadata(0, new List<Expr>());
TheAssert.GetMetadata<List<Expr>>(0);
foreach (var keyValue in TheAssert.NumberedMetaData)
{
// do something
}
Debug.Assert(TheAssert.NumberedMetaDataCount == 1);
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
true but A.GetHashCode() == B.GetHashCode() return false.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
BinderExpr was doing:
object.Equals(this.TypeParameters, other.TypeParameters)
&& object.Equals(this.Dummies, other.Dummies)
Both of these are wrong because these are of type List<> and so
- object.Equals(this.TypeParamters, other.TypeParameters) will call this.TypeParameters.Equals(other.TypeParamters) (assuming they aren't references to the same list)
- object.Equals(this.Dummies, other.TypeParameters) will call this.TypeParameters.Equals(other.Dummies) (assuming they aren't references to the same list)
so this is becomes a reference comparision on Lists<>. This is wrong
because Equals() has been overloaded to implement structural equality.
This affects the classes ForallExpr, LambdaExpr and ExistsExpr.
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |/ |
|
| |/
|
|
| |
the StdDispatch method was missing on both Classes.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
computing statement checksums).
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
advanced verification result caching even for implementations with errors.
|
| |
|
|
| |
injected by the verification result caching for calls within loops.
|
| |
|
|
| |
preconditions.
|
| |
|
|
| |
verification result caching.
|
| | |
|
| |
|
|
|
|
| |
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.
|
wuestholz
Dan Liew
Dan Rosén