| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
| |
existential if guards.
Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.
|
| |
|
|
| |
Moved all bounds discovery to resolution pass 1.
|
| |
|
|
|
|
| |
pass 0.
Fixed resolution of specification components of alternative loops.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
and #module were not handled
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Although
convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported. This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior. For auto-declare, identifiers could be used in the program
without having a declaration. For fill-in parameters, the implicitly declared
type parameters remain anonymous.
|
| | |
|
| |
|
|
| |
have a unique value
|
| |
|
|
| |
Fixed comments in some test cases.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
| | |
|
| |
|
|
|
|
| |
appearing in reads clauses.
Fixed bug in the checking of reads subset for field frame targets ("back ticks")
|
| |
|
|
| |
declarations
|
| |
|
|
|
|
| |
Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it).
If the type of literal "null" is unresolved, make the type "object".
The need to translate unresolved proxies is now assumed to be gone.
|
| |
|
|
|
| |
Arbitrary conversion from int/real to derived types not yet supported.
Changed rules about numeric type conversions to allow conversions from any numeric type.
|
| |\ |
|
| | |
| |
| |
| | |
Fixed bug in type checking for integer division.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now, loops that may possibly
do an infinite number of iterations (that is, loops marked with 'decreases *') and calls to methods
marked with 'decreases *' are allowed only in methods that themselves are marked with 'decreases *'. As
before, ghost loops and ghost methods are not allowed to be marked with 'decreases *'.
Previously, 'decreases *' was allowed on a method only if the method was tail recursive;
this is no longer so. Note, however, that if the method is not tail recursive and engages
in infinite recursion, then it will eventually run out of stack space.
Previously, a 'decreases *' was not inherited in a refining module; this is no longer so.
That is, 'decreases *' is now inherited. To refine a possibly non-terminating method
or loop, the refining version simply provides a decreases clause that does not mention '*'.
Note that if the refined method is not recursive, it still needs to have _some_ decreases
clause in order not to inherit the 'decreases *' from the refined method, but the expression
stated in the decreases clause can be arbitrary (for example, one can write 'decreases true'
or 'decreases 7' or 'decreases x' for some 'x' in scope).
Note, in the new design, a method needs to be declared with 'decreases *' if
it may recurse forever _or_ if it contains a possibly infinite loop.
Note that the absence of 'decreases *' on a loop does not mean the loop will
terminate, but it does mean that the loop will iterate a finite number of times
(the subtle distinction here is that a loop without a 'decreases *' is allowed
to contain a nested loop that has a 'decreases *' -- provided the enclosing
method is also declared with 'decreases *', as previously mentioned).
|
| |
|
|
| |
twoState and codeContext is moved to a new class ResolveOpts
|
| | |
|
| |
|
|
| |
the resolver and translator
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
| |
Enhanced filling in of datatype parameters: allow places that need only a prefix of the parameters of the datatype
|
| |
|
|
| |
around a comma-delimited list of expressions or types. Unit and the unit type are denoted ().
|
| |
|
|
|
|
|
|
|
|
|
| |
One can now write forall statements without bodies
(but with ensures clauses) as follows:
forall s | s in S ensures s < 0;
where S is set<int>.
The ensures clauses are assumed but not checked.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
|
| |
|
|
| |
Improved situation with (reducing bogosity of) type checking of "object".
|
| | |
|
| | |
|
| |
|
|
| |
be done: replace InMethodContext with a Function/Method-Height in translator.)
|
| |
|
|
| |
a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
|
| |
|
|
|
|
|
| |
where more type information is known
Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.
|
| | |
|
| | |
|
Rustan Leino
Dan Rosén
Nadia Polikarpova