| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
it. Don't use pretty warning signs since we can't diff them correctly in the
test output from the test run.
|
| |
|
|
|
| |
Window's batch doesn't recognize ";" as a command separator; lit has a
workaround for that, bu it's just as simple to do the right thing on our side.
|
| |
|
|
| |
have a unique value
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
| |
of a match expression).
Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator.
Fixed compilation of match expressions, to allow them anywhere.
|
| | |
|
| |
|
|
| |
around the bound variables optional.
|
| |
|
|
| |
be used
|
| | |
|
|
|
Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression)
Dafny: various implementation clean-ups
|
qunyanm
Clément Pit--Claudel
Rustan Leino