Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
e5d3e35e
Commit
e5d3e35e
authored
Mar 18, 2011
by
Jean-Christophe Filliâtre
Browse files
fixed label precedence in programs
parent
8e58285e
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/parser/parser.pre.mly
View file @
e5d3e35e
...
...
@@ -190,6 +190,7 @@
/*
Precedences
*/
%
nonassoc
prec_label
%
nonassoc
prec_post
%
nonassoc
BAR
...
...
@@ -1073,7 +1074,7 @@ expr:
{
mk_expr
(
Ematch
(
$
2
,
$
5
))
}
|
MATCH
expr
COMMA
list1_expr_sep_comma
WITH
bar_
program_match_cases
END
{
mk_expr
(
Ematch
(
mk_expr
(
Etuple
(
$
2
::$
4
))
,
$
7
))
}
|
LABEL
uident
COLON
expr
|
LABEL
uident
COLON
expr
%
prec
prec_label
{
mk_expr
(
Elabel
(
$
2
,
$
4
))
}
|
LOOP
loop_annotation
expr
END
{
mk_expr
(
Eloop
(
$
2
,
$
3
))
}
...
...
src/programs/TODO
View file @
e5d3e35e
o automatically add a label pre_f at entrance of each function f
o use of old in loop invariant should be reported as an error (correctly)
o what about pervasives old, at, label, unit = ()
...
...
@@ -7,8 +9,6 @@ o what about pervasives old, at, label, unit = ()
o fmla_effect
o fixed precedence of label (label L: e) wrt sequence (e ; e)
o model types (abstract but not mutable)
abstract types (no model)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment