| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
type exist. This remains a work in progress
|
| |
|
|
|
| |
negative numbers. I have decided that this method will floor towards
negative infinity rather than zero to match SMT-LIBv2's to_int function.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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
|
| |
|
|
|
| |
required changing the line endings so that it uses unix
line endings.
|
|
|
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