| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
bitvector values
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
require later modification
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
of its methods now demand the return value to equal the given node.
Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
which says that a function is an identity function.
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
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).
|
| |
|
|
| |
see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
Expr's, not the more abstract AIExpr's.
Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false.
Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals
Boogie: Mark all inferred conditions with attribute {:inferred}
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
|
| |
|
|
| |
Select 4.0 client profile on all projects
|
| |
|
|
|
|
| |
files generated by Coco/R.
This was done to support sharing of the Coco/R .frame files with Spec#.
|
| | |
|
| |
|
|
| |
Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
|
| | |
|
| |
|
|
|
| |
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.
|
| |
|
|
| |
fewer error messages when compiling with runtime checking on.
|
| |
|
|
| |
doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
|
| |
|
|
| |
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.
|
| | |
|
Checkmate50
Dan Liew
wuestholz
Pantazis Deligiannis
Ken McMillan
Rustan Leino
qadeer