Skip to content
GitLab
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
cc748e4f
Commit
cc748e4f
authored
Oct 15, 2018
by
Andrei Paskevich
Browse files
Parser: fix erroneous variable redefinition
thanks to Sylvain for noticing.
parent
2c43796b
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/parser/parser.mly
View file @
cc748e4f
...
...
@@ -969,8 +969,8 @@ single_expr_:
let
e
=
{
e
with
expr_desc
=
Ewhile
(
e1
,
inv
,
var
,
cont
e2
)
}
in
let
id
=
{
id
with
id_str
=
id
.
id_str
^
break_id
}
in
Eoptexn
(
id
,
Ity
.
MaskVisible
,
e
)
|
Efor
(
i
d
,
ef
,
dir
,
et
,
inv
,
e1
)
->
let
e
=
{
e
with
expr_desc
=
Efor
(
i
d
,
ef
,
dir
,
et
,
inv
,
cont
e1
)
}
in
|
Efor
(
i
,
ef
,
dir
,
et
,
inv
,
e1
)
->
let
e
=
{
e
with
expr_desc
=
Efor
(
i
,
ef
,
dir
,
et
,
inv
,
cont
e1
)
}
in
let
id
=
{
id
with
id_str
=
id
.
id_str
^
break_id
}
in
Eoptexn
(
id
,
Ity
.
MaskVisible
,
e
)
|
d
->
d
in
...
...
@@ -981,7 +981,7 @@ single_expr_:
let
e
=
{
$
5
with
expr_desc
=
Eoptexn
(
id_c
,
Ity
.
MaskVisible
,
$
5
)
}
in
let
e
=
mk_expr
(
Ewhile
(
$
2
,
fst
$
4
,
snd
$
4
,
e
))
$
startpos
$
endpos
in
Eoptexn
(
id_b
,
Ity
.
MaskVisible
,
e
)
}
|
FOR
lident_nq
EQUAL
seq_expr
for_dir
ection
seq_expr
DO
invariant
*
loop_body
DONE
|
FOR
lident_nq
EQUAL
seq_expr
for_dir
seq_expr
DO
invariant
*
loop_body
DONE
{
let
id_b
=
mk_id
break_id
$
startpos
(
$
7
)
$
endpos
(
$
7
)
in
let
id_c
=
mk_id
continue_id
$
startpos
(
$
7
)
$
endpos
(
$
7
)
in
let
e
=
{
$
9
with
expr_desc
=
Eoptexn
(
id_c
,
Ity
.
MaskVisible
,
$
9
)
}
in
...
...
@@ -1100,7 +1100,7 @@ assertion_kind:
|
ASSUME
{
Expr
.
Assume
}
|
CHECK
{
Expr
.
Check
}
for_dir
ection
:
for_dir
:
|
TO
{
Expr
.
To
}
|
DOWNTO
{
Expr
.
DownTo
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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