| 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.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
| |
added another test in linear (based on bug reported by Chris)
removed the QED build configuration
|
| |
|
| |
|
|
|
|
| |
functionality.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
- moved doomed and predication code into separate projects;
for doomed there is a static dependency from BoogieDriver
but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
|
|
|
|
|
|
|
| |
interval-based abstract interpretation instead.
Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie.
Command-line option '/logInfer' has been dropped.
|
| |
|
|
|
|
|
| |
also changing back the output path in BoogieDriver
also disabling z3api for now since it does not build
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Should not affect function
of other provers. There is an option added in Check.cs to allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).
|
|/
|
|
| |
removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
|
| |
|
|
|
|
|
|
| |
files generated by Coco/R.
This was done to support sharing of the Coco/R .frame files with Spec#.
|
| |
|
| |
|
| |
|
|
|
|
|
| |
only this target has a compile time dependency on Microsoft.Z3.dll.
To compile this target, a reference to z3api must be manually added to BoogieDriver.
|
|
|
|
| |
project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
|
| |
|
|
|
|
| |
Z3api.csproj shouldn't get in the way this time 'round.
|
|
|
|
| |
files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
|
|
|
|
| |
Core to jive with recent changes made to the cce class.
|
| |
|
|
|
|
| |
Microsoft.Z3.dll and to C#. It does not work yet.
|
| |
|
|
|
|
| |
Don't insist on DafnyDriver picking up the LKG version (1.0.21125.0) of the Spec# runtime (in fact, most builders will probably have 1.0.21126.0).
|
|
|
|
| |
project; making Core work with the port by removing the nonnull requirements on one abstract method.
|
|
|
|
| |
references of simplify's dependents.
|
| |
|
| |
|
|
|
|
|
|
| |
regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL.
Address any error complaints to t-abarbe@microsoft.com
|
| |
|
|
|
|
|
|
|
| |
changes made to the .csproj and Boogie.sln file that are necessary for the port.
My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me.
</BoogieDriver> </Boogie>
|
|
|
|
| |
/stratifiedInline:1.
|
| |
|
|
|