| 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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| | |
|
| | |
|
| |
|
|
|
| |
Previously after duplication of an entire program CallCmd.Proc would
point to procedures in the old program.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Daniel Liew.
|
| |
|
|
|
|
| |
before real verification.
Fixed treatment of lambda-expression attributes.
|
| | |
|
| |
|
|
| |
optimized the FailurePreservationChecker to eliminate some quantifiers
|
| |
|
|
| |
other bug fixes in QED stuff
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
conversion from Spec# into C# moved a constructor call
|
| | |
|
| |
|
Dan Liew
Valentin Wüstholz
wuestholz
Unknown
Unknown