| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| |
|
|
| |
Moved all bounds discovery to resolution pass 1.
|
| | |
|
| |
|
|
|
|
|
| |
Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
clues about which parameters to include.
As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.
|
| |
|
|
|
|
| |
time) in the test suite.
Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do.
|
| |
|
|
|
|
|
|
|
| |
Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we
print tokens, we need to decrement the column number. This was done for resolver
errors, but not for verification or parsing errors. In addition, parsing errors
were inconsistent with resolution errors case-wise.
Unfortunately, the fix affects the output of many tests.
|
| |\
| |
| |
| |
| | |
This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.
|
| | | |
|
| | |
| |
| |
| | |
Found by enabling auto-generated triggers and looking for failing tests
|
| | | |
|
| | |\ |
|
| |/ /
| |
| |
| | |
Improvements in encoding of reads of function values.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
i.e., how many times Z3 is permitted to unfold it's definition. The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume. The general format is:
{:fuel functionName,lowFuel,highFuel}
When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.
The default fuel setting for recursive functions is 1,2. Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care. Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
| |
The problem was this:
Console.WriteLine(Int64.Parse("08000000000000000", NumberStyles.HexNumber));
// => -9223372036854775808
Console.WriteLine(Int64.Parse("9223372036854775808"));
// => Value was either too large or too small for an Int64.
In other words, large hex numbers are interpreted as a sequence of bits, not as
an actual number.
|
| | |
|
| |
|
|
| |
need for Total
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Fix bug with not seeing imap's because of type synonyms.
Don't show semi-colon after "decreases" in hover text.
Minor cosmetic change in a test case.
|
| |
|
|
|
|
| |
Klein book on semantics.
It includes many uses of inductive predicates and inductive lemmas.
|
| |
|
|
| |
Klein book on semantics
|
| | |
|
| |
|
|
| |
function has a MemberSelectExpr that accesses a type with only one constructor.
|
| | |
|
| | |
|
| |
|
|
| |
members of the enclosing module or its imports.
|
| |
|
|
| |
elements.
|
| | |
|
| |
|
|
| |
fn in fixupRevealLemma substitute the types as well.
|
| | |
|
| |
|
|
| |
or == for equality testing.
|
| |
|
|
| |
class when determining whether a method named Main() is the program entry.
|
| |
|
|
| |
dontCareAboutCompilation flag should be set to false in the ResolveOpts.
|
| |
|
|
| |
instead of FunctionCall.
|
| |
|
|
| |
call.
|
| | |
|
| |
|
|
|
|
| |
F's corresponding F_FULL, make sure the function is indeed the FullVesion
before the substitution. Also keep the TypeArgsSubst for the enclosingClass in
the typeMap.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
| |
outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'.
Semantics of 'protected':
* The definition (i.e., body) of a 'protected' function is not visible outside the defining module
* The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions.
* In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected'
* The 'protected' status of a function must be preserved in refinement modules
|
| | |
|
Rustan Leino
Clément Pit--Claudel
Bryan Parno