jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Remove controllables from parser

Browse source
This commit is contained in:
Cédric Pasteur 2010-07-16 16:08:14 +02:00
parent aeca344db5
commit fac69ac2fa
2 changed files with 2 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
compiler/heptagon/parsing/hept_parser.mly
View file

@ -206,12 +206,11 @@ node_params:
contract:
| /* empty */ {None}
| CONTRACT loc_vars opt_equs opt_assume enforce opt_with
| CONTRACT loc_vars opt_equs opt_assume enforce
{Some{c_local = $2;
c_eq = $3;
c_assume = $4;
c_enforce = $5;
c_controllables = $6 }}
c_enforce = $5 }}
;
opt_equs:
@ -228,11 +227,6 @@ enforce:
| ENFORCE exp { $2 }
;
opt_with:
| /* empty */ { [] }
| WITH LPAREN params RPAREN { $3 }
;
loc_vars:
| /* empty */ { [] }
| VAR loc_params { $2 }

1
compiler/heptagon/parsing/hept_parsetree.ml
View file

@ -115,7 +115,6 @@ and type_desc =
type contract =
{ c_assume : exp;
c_enforce : exp;
c_controllables : var_dec list;
c_local : var_dec list;
c_eq : eq list;
}