| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
variable that begins with a ``.``. This was't an issue for Z3 which
ignores this but CVC4 is stricter and will emit an error
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Drop the “basic” block predication algorithm. Block predication is only used
by GPUVerify, and then only in the “smart” version as the basic algorithm does
not perform very well. As a consequence this code is essentially dead.
|
| | |
|
| |
|
|
| |
Expose information about the predicate assigned to the immediate dominator of a CFG node.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
otherwise if either of the following happens
* if the solver hangs and we do CTRL+C
* if Boogie crashes
then some lines will be missing from the log.
|
| |
|
|
|
|
| |
where setting produce-unsat-cores to true has no effect unless the option is set last.
This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2
|
| |
|
|
|
| |
negative numbers. I have decided that this method will floor towards
negative infinity rather than zero to match SMT-LIBv2's to_int function.
|
| |
|
|
| |
DoModSetAnalysis needs to run before the linear and mover type checking.
|
| | |
|
| |
|
|
|
| |
taken from ``bv_decl_plugin::get_op_names(...)`` in
``src/ast/bv_decl_plugin.cpp`` in the Z3 4.3.2 source code.
|
| |
|
|
|
|
|
| |
taken
from `` arith_decl_plugin::get_op_names(...)`` from ``src/ast/arith_decl_plugin.cpp``
in the Z3 4.3.2 source code.
|
| |
|
|
|
| |
from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp``
from the Z3 4.3.2 source code.
|
| |\ |
|
| | |
| |
| |
| | |
when generating the VC.
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
Compilation does not depend NUnit.Runners so it should not be
a required package. Instead users should install it manually as
described in Source/UnitTests/README.md
|
| |
|
|
|
|
| |
attempt to unbreak the Jenkins build. I don't think doing this
is ideal. The package isn't required to run tests, it's only required
if you want to run them on the command line.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
out we had the repository set up in "MSBuild-Integrated package" mode[1]
(missing packages won't fetched unless the user explicitly allows it for the
solution) but what we want is "Automatic package restore" (provided NuGet is
setup correctly automatically fetch the missing packages). I've followed the
migration guide [2] and it appears that now Visual Studio will try to
automatically fetch after making this change.
[1] http://docs.nuget.org/consume/package-restore
[2] http://docs.nuget.org/Consume/Package-Restore/Migrating-to-Automatic-Package-Restore
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
akashlal
Valentin Wüstholz
Dan Liew
Akash Lal
qadeer
akashlal