Skip to content
Snippets Groups Projects
Commit eb26b100 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[parser] first steps for removing menhir-incompatible lexer hacks 

- full_identifier accepts non-c keywords (list to be completed)
- logic_type rule is parameterized by the kind of typenames we accept
  (either only typenames or typenames + identifiers for rt_type
- on the other hand, logic_attributes cannot have the same name as
  an ACSL keyword.
parent c7cefd9f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_internals/parsing/logic_parser.mly
+ 109
− 183
View file @ eb26b100
...@@ -96,14 +96,6 @@ ...@@ -96,14 +96,6 @@
let l = Stack.pop type_variables_stack in let l = Stack.pop type_variables_stack in
List.iter Logic_env.remove_typename l List.iter Logic_env.remove_typename l
let rt_type = ref false
let set_rt_type () = rt_type:= true
let reset_rt_type () = rt_type:=false
let is_rt_type () = !rt_type
let loc_decl start_end d = { decl_node = d; decl_loc = loc start_end } let loc_decl start_end d = { decl_node = d; decl_loc = loc start_end }
let loc_ext start_end d = { extended_node = d; extended_loc = loc start_end } let loc_ext start_end d = { extended_node = d; extended_loc = loc start_end }
...@@ -338,29 +330,6 @@ ...@@ -338,29 +330,6 @@
%% %%
enter_kw_c_mode:
| /* empty */ { enter_kw_c_mode () }
;
exit_kw_c_mode:
| /* empty */ { exit_kw_c_mode () }
;
enter_rt_type:
| /* empty */ { if is_rt_type () then enter_rt_type_mode () }
;
exit_rt_type:
| /* empty */ { if is_rt_type () then exit_rt_type_mode () }
;
begin_rt_type:
| /* empty */ { set_rt_type () }
end_rt_type:
| /* empty */ { reset_rt_type () }
;
/*** predicates and terms ***/ /*** predicates and terms ***/
lexpr_list: lexpr_list:
...@@ -374,7 +343,7 @@ ne_lexpr_list: ...@@ -374,7 +343,7 @@ ne_lexpr_list:
; ;
lexpr_eof: lexpr_eof:
| full_lexpr EOF { $1 } | lexpr EOF { $1 }
; ;
lexpr_option: lexpr_option:
...@@ -544,8 +513,8 @@ lexpr_inner: ...@@ -544,8 +513,8 @@ lexpr_inner:
| lexpr_inner SLASH lexpr_inner { info $sloc (PLbinop ($1, Bdiv, $3)) } | lexpr_inner SLASH lexpr_inner { info $sloc (PLbinop ($1, Bdiv, $3)) }
| lexpr_inner PERCENT lexpr_inner { info $sloc (PLbinop ($1, Bmod, $3)) } | lexpr_inner PERCENT lexpr_inner { info $sloc (PLbinop ($1, Bmod, $3)) }
| lexpr_inner STARHAT lexpr_inner { info $sloc (PLrepeat ($1, $3)) } | lexpr_inner STARHAT lexpr_inner { info $sloc (PLrepeat ($1, $3)) }
| lexpr_inner ARROW identifier_or_typename { info $sloc (PLarrow ($1, $3)) } | lexpr_inner ARROW identifier_or_typename_full { info $sloc (PLarrow ($1, $3)) }
| lexpr_inner DOT identifier_or_typename { info $sloc (PLdot ($1, $3)) } | lexpr_inner DOT identifier_or_typename_full { info $sloc (PLdot ($1, $3)) }
| lexpr_inner LSQUARE range RSQUARE { info $sloc (PLarrget ($1, $3)) } | lexpr_inner LSQUARE range RSQUARE { info $sloc (PLarrget ($1, $3)) }
| lexpr_inner LSQUARE lexpr RSQUARE { info $sloc (PLarrget ($1, $3)) } | lexpr_inner LSQUARE lexpr RSQUARE { info $sloc (PLarrget ($1, $3)) }
| LSQUAREPIPE lexpr_list RSQUAREPIPE { info $sloc (PLlist $2) } | LSQUAREPIPE lexpr_list RSQUAREPIPE { info $sloc (PLlist $2) }
...@@ -561,13 +530,13 @@ lexpr_inner: ...@@ -561,13 +530,13 @@ lexpr_inner:
| RESULT { info $sloc PLresult } | RESULT { info $sloc PLresult }
| SEPARATED LPAR ne_lexpr_list RPAR | SEPARATED LPAR ne_lexpr_list RPAR
{ info $sloc (PLseparated $3) } { info $sloc (PLseparated $3) }
| identifier LPAR ne_lexpr_list RPAR | full_identifier LPAR ne_lexpr_list RPAR
{ info $sloc (PLapp ($1, [], $3)) } { info $sloc (PLapp ($1, [], $3)) }
| identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR | full_identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
{ info $sloc (PLapp ($1, $3, $6)) } { info $sloc (PLapp ($1, $3, $6)) }
| identifier LBRACE ne_label_args RBRACE | full_identifier LBRACE ne_label_args RBRACE
{ info $sloc (PLapp ($1, $3, [])) } { info $sloc (PLapp ($1, $3, [])) }
| identifier { info $sloc (PLvar $1) } | full_identifier { info $sloc (PLvar $1) }
| PI { info $sloc (PLvar "\\pi") } | PI { info $sloc (PLvar "\\pi") }
| lexpr_inner GTGT lexpr_inner { info $sloc (PLbinop ($1, Brshift, $3))} | lexpr_inner GTGT lexpr_inner { info $sloc (PLbinop ($1, Brshift, $3))}
| lexpr_inner LTLT lexpr_inner { info $sloc (PLbinop ($1, Blshift, $3))} | lexpr_inner LTLT lexpr_inner { info $sloc (PLbinop ($1, Blshift, $3))}
...@@ -576,8 +545,8 @@ lexpr_inner: ...@@ -576,8 +545,8 @@ lexpr_inner:
| LPAR cast_logic_type RPAR lexpr_inner %prec prec_cast | LPAR cast_logic_type RPAR lexpr_inner %prec prec_cast
{ info $sloc (PLcast ($2, $4)) } { info $sloc (PLcast ($2, $4)) }
| TYPEOF LPAR lexpr RPAR { info $sloc (PLtypeof $3) } | TYPEOF LPAR lexpr RPAR { info $sloc (PLtypeof $3) }
| BSTYPE LPAR type_spec RPAR { info $sloc (PLtype $3) } | BSTYPE LPAR type_spec(typename) RPAR { info $sloc (PLtype $3) }
| BSTYPE LPAR type_spec stars RPAR { info $sloc (PLtype ($4 $3)) } | BSTYPE LPAR type_spec(typename) stars RPAR { info $sloc (PLtype ($4 $3)) }
/* tsets */ /* tsets */
| EMPTY { info $sloc PLempty } | EMPTY { info $sloc PLempty }
| BSUNION LPAR lexpr_list RPAR { info $sloc (PLunion $3) } | BSUNION LPAR lexpr_list RPAR { info $sloc (PLunion $3) }
...@@ -601,8 +570,8 @@ lexpr_inner: ...@@ -601,8 +570,8 @@ lexpr_inner:
; ;
ne_label_args: ne_label_args:
| identifier_or_typename { [ $1 ] } | identifier_or_typename_full { [ $1 ] }
| identifier_or_typename COMMA ne_label_args { $1 :: $3 } | identifier_or_typename_full COMMA ne_label_args { $1 :: $3 }
string: string:
| STRING_LITERAL { $1 } | STRING_LITERAL { $1 }
...@@ -620,7 +589,7 @@ range: ...@@ -620,7 +589,7 @@ range:
/*** Aggregated object initialization ***/ /*** Aggregated object initialization ***/
field_path_elt: field_path_elt:
| DOT identifier_or_typename { $2 } | DOT identifier_or_typename_full { $2 }
; ;
field_init_elt: field_init_elt:
| field_path_elt EQUAL lexpr { ($1, $3) } | field_path_elt EQUAL lexpr { ($1, $3) }
...@@ -686,7 +655,7 @@ binders_reentrance: ...@@ -686,7 +655,7 @@ binders_reentrance:
; ;
decl_spec: decl_spec:
| type_spec var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) } | type_spec(typename) var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) }
; ;
var_spec: var_spec:
...@@ -745,50 +714,50 @@ abs_param: ...@@ -745,50 +714,50 @@ abs_param:
| logic_type { $1 } | logic_type { $1 }
; ;
/*** restricted type expressions ***/
id_as_typename:
| identifier { LTnamed($1, []) }
;
ne_parameters: ne_parameters:
| parameter { [$1] } | parameter { [$1] }
| parameter COMMA ne_parameters { $1 :: $3 } | parameter COMMA ne_parameters { $1 :: $3 }
; ;
parameter: parameter:
| type_spec var_spec { let (modif, name) = $2 in (modif $1, name)} | type_spec(identifier_or_typename) var_spec
| id_as_typename var_spec { let (modif, name) = $2 in (modif $1, name) } { let (modif, name) = $2 in (modif $1, name)}
; ;
/*** type expressions ***/ /*** type expressions ***/
logic_type: logic_type_gen(tname):
| type_spec abs_spec_option { $2 $1 } | type_spec(tname) abs_spec_option { $2 $1 }
; ;
typename:
| name = TYPENAME { name }
/* TODO treat the case of an ACSL keyword that is also a typedef */
;
logic_type: logic_type_gen(typename) { $1 }
cv: cv:
CONST { cv_const } CONST { cv_const }
| VOLATILE { cv_volatile } | VOLATILE { cv_volatile }
| BSGHOST { cv_ghost } | BSGHOST { cv_ghost }
; ;
type_spec_cv: type_spec_cv(tname):
type_spec cv_after { $2 $1 } type_spec(tname) cv_after { $2 $1 }
| cv type_spec_cv { LTattribute ($2, $1) } | cv type_spec_cv(tname) { LTattribute ($2, $1) }
cv_after: cv_after:
/* empty */ { fun t -> t } /* empty */ { fun t -> t }
| cv cv_after { fun t -> $2 (LTattribute (t,$1)) } | cv cv_after { fun t -> $2 (LTattribute (t,$1)) }
cast_logic_type: cast_logic_type:
| type_spec_cv abs_spec_cv_option { $2 $1 } | type_spec_cv(TYPENAME) abs_spec_cv_option { $2 $1 }
; ;
logic_rt_type: logic_rt_type:
| id_as_typename { $1 } | logic_type_gen(identifier_or_typename) { $1 }
| begin_rt_type logic_type end_rt_type { $2 }
; ;
abs_spec_option: abs_spec_option:
...@@ -854,7 +823,7 @@ tabs: ...@@ -854,7 +823,7 @@ tabs:
} }
; ;
type_spec: type_spec(tname):
| INTEGER { LTinteger } | INTEGER { LTinteger }
| REAL { LTreal } | REAL { LTreal }
| BOOLEAN { LTnamed (Utf8_logic.boolean,[]) } | BOOLEAN { LTnamed (Utf8_logic.boolean,[]) }
...@@ -894,63 +863,23 @@ type_spec: ...@@ -894,63 +863,23 @@ type_spec:
| FLOAT { LTfloat FFloat } | FLOAT { LTfloat FFloat }
| DOUBLE { LTfloat FDouble } | DOUBLE { LTfloat FDouble }
| LONG DOUBLE { LTfloat FLongDouble } | LONG DOUBLE { LTfloat FLongDouble }
| STRUCT exit_rt_type identifier_or_typename { LTstruct $3 } | STRUCT id = identifier_or_typename_full { LTstruct id }
| ENUM exit_rt_type identifier_or_typename { LTenum $3 } | ENUM id = identifier_or_typename_full { LTenum id }
| UNION exit_rt_type identifier_or_typename { LTunion $3 } | UNION id = identifier_or_typename_full { LTunion id }
| TYPENAME { LTnamed ($1,[]) } | name = tname { LTnamed (name,[]) }
| TYPENAME LT enter_rt_type ne_logic_type_list GT exit_rt_type | name = tname LT prms = ne_logic_type_list(tname) GT { LTnamed(name,prms) }
{ LTnamed($1,$4) }
; ;
ne_logic_type_list: ne_logic_type_list(tname):
| logic_type { [$1] } | l = separated_nonempty_list(COMMA,logic_type_gen(tname)) { l }
| logic_type COMMA enter_rt_type ne_logic_type_list { $1 :: $4 }
; ;
/*** from annotations ***/ /*** from annotations ***/
full_lexpr:
| enter_kw_c_mode lexpr exit_kw_c_mode { $2 }
;
full_identifier: full_identifier:
| enter_kw_c_mode identifier exit_kw_c_mode { $2 } | id = identifier { id }
; | CHECK { "check" }
| id = EXT_CODE_ANNOT { id }
full_identifier_or_typename:
| enter_kw_c_mode identifier_or_typename exit_kw_c_mode { $2 }
;
full_parameters:
| enter_kw_c_mode ne_parameters exit_kw_c_mode { $2 }
;
full_parameter:
| enter_kw_c_mode parameter exit_kw_c_mode { $2 }
;
full_zones:
| enter_kw_c_mode zones exit_kw_c_mode { $2 }
;
full_ne_zones:
| enter_kw_c_mode ne_zones exit_kw_c_mode { $2 }
;
full_ne_lexpr_list:
enter_kw_c_mode ne_lexpr_list exit_kw_c_mode { $2 }
;
full_logic_type:
| enter_kw_c_mode logic_type exit_kw_c_mode { $2 }
;
full_logic_rt_type:
| enter_kw_c_mode logic_rt_type exit_kw_c_mode { $2 }
;
full_assigns:
| enter_kw_c_mode assigns exit_kw_c_mode { $2 }
; ;
/*** ACSL extension for external spec file ***/ /*** ACSL extension for external spec file ***/
...@@ -971,8 +900,8 @@ ext_global_clauses: ...@@ -971,8 +900,8 @@ ext_global_clauses:
ext_global_clause: ext_global_clause:
| decl { Ext_decl (loc_decl $sloc $1) } | decl { Ext_decl (loc_decl $sloc $1) }
| EXT_LET any_identifier EQUAL full_lexpr SEMICOLON { Ext_macro (false, $2, $4) } | EXT_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (false, $2, $4) }
| GLOBAL EXT_LET any_identifier EQUAL full_lexpr SEMICOLON { Ext_macro (true, $3, $5) } | GLOBAL EXT_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (true, $3, $5) }
| INCLUDE string SEMICOLON { let b,s = $2 in Ext_include(b,s, loc $sloc) } | INCLUDE string SEMICOLON { let b,s = $2 in Ext_include(b,s, loc $sloc) }
; ;
...@@ -1183,12 +1112,12 @@ requires: ...@@ -1183,12 +1112,12 @@ requires:
; ;
ne_requires: ne_requires:
| REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Assert $2::$4 } | REQUIRES lexpr SEMICOLON requires { toplevel_pred Assert $2::$4 }
| CHECK_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Check $2 :: $4 } | CHECK_REQUIRES lexpr SEMICOLON requires { toplevel_pred Check $2 :: $4 }
| ADMIT_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Admit $2 :: $4 } | ADMIT_REQUIRES lexpr SEMICOLON requires { toplevel_pred Admit $2 :: $4 }
| REQUIRES full_lexpr clause_kw { missing $loc($2) ";" $3 } | REQUIRES lexpr clause_kw { missing $loc($2) ";" $3 }
| CHECK_REQUIRES full_lexpr clause_kw { missing $loc($2) ";" $3 } | CHECK_REQUIRES lexpr clause_kw { missing $loc($2) ";" $3 }
| ADMIT_REQUIRES full_lexpr clause_kw { missing $loc($2) ";" $3 } | ADMIT_REQUIRES lexpr clause_kw { missing $loc($2) ";" $3 }
; ;
terminates: terminates:
...@@ -1197,8 +1126,8 @@ terminates: ...@@ -1197,8 +1126,8 @@ terminates:
; ;
ne_terminates: ne_terminates:
| TERMINATES full_lexpr SEMICOLON { $2 } | TERMINATES lexpr SEMICOLON { $2 }
| TERMINATES full_lexpr clause_kw { missing $loc($2) ";" $3 } | TERMINATES lexpr clause_kw { missing $loc($2) ";" $3 }
; ;
decreases: decreases:
...@@ -1212,8 +1141,8 @@ ne_decreases: ...@@ -1212,8 +1141,8 @@ ne_decreases:
; ;
variant: variant:
| full_lexpr FOR any_identifier { ($1, Some $3) } | lexpr FOR any_identifier { ($1, Some $3) }
| full_lexpr { ($1, None) } | lexpr { ($1, None) }
; ;
simple_clauses: simple_clauses:
...@@ -1222,11 +1151,11 @@ simple_clauses: ...@@ -1222,11 +1151,11 @@ simple_clauses:
; ;
allocation: allocation:
| ALLOCATES full_zones { FreeAlloc([],$2) } | ALLOCATES zones { FreeAlloc([],$2) }
| FREES full_zones { FreeAlloc($2,[]) } | FREES zones { FreeAlloc($2,[]) }
ne_simple_clauses: ne_simple_clauses:
| post_cond_kind full_lexpr SEMICOLON simple_clauses | post_cond_kind lexpr SEMICOLON simple_clauses
{ let tp_kind, kind = $1 in { let tp_kind, kind = $1 in
let allocation,assigns,post_cond,extended = $4 in let allocation,assigns,post_cond,extended = $4 in
allocation,assigns, allocation,assigns,
...@@ -1236,31 +1165,27 @@ ne_simple_clauses: ...@@ -1236,31 +1165,27 @@ ne_simple_clauses:
let a = concat_allocation allocation $1 in let a = concat_allocation allocation $1 in
a,assigns,post_cond,extended a,assigns,post_cond,extended
} }
| ASSIGNS full_assigns SEMICOLON simple_clauses | ASSIGNS assigns SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $4 in { let allocation,assigns,post_cond,extended = $4 in
let a = concat_assigns $sloc assigns $2 let a = concat_assigns $sloc assigns $2
in allocation,a,post_cond,extended in allocation,a,post_cond,extended
} }
| EXT_CONTRACT grammar_extension SEMICOLON simple_clauses | EXT_CONTRACT extension_content SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $4 in { let allocation,assigns,post_cond,extended = $4 in
let processed = Logic_env.preprocess_extension $1 $2 in let processed = Logic_env.preprocess_extension $1 $2 in
allocation,assigns,post_cond,($1,processed)::extended allocation,assigns,post_cond,($1,processed)::extended
} }
| post_cond_kind full_lexpr clause_kw { missing $loc($2) ";" $3 } | post_cond_kind lexpr clause_kw { missing $loc($2) ";" $3 }
| allocation clause_kw { missing $loc($1) ";" $2 } | allocation clause_kw { missing $loc($1) ";" $2 }
| ASSIGNS full_assigns clause_kw { missing $loc($2) ";" $3 } | ASSIGNS assigns clause_kw { missing $loc($2) ";" $3 }
| EXT_CONTRACT ne_grammar_extension clause_kw { missing $loc($1) ";" $3 } | EXT_CONTRACT ne_grammar_extension clause_kw { missing $loc($1) ";" $3 }
; ;
ne_grammar_extension: ne_grammar_extension:
| full_zones { $1 } | zones { $1 }
; ;
/* possibly empty list of terms, for ACSL extensions registered by plugins. */ /* possibly empty list of terms, for ACSL extensions registered by plugins. */
grammar_extension:
| enter_kw_c_mode extension_content exit_kw_c_mode { $2 }
;
extension_content: extension_content:
| /* epsilon */ { [] } | /* epsilon */ { [] }
| zones { $1 } | zones { $1 }
...@@ -1298,8 +1223,8 @@ behavior_body: ...@@ -1298,8 +1223,8 @@ behavior_body:
assumes: assumes:
| /* epsilon */ { [] } | /* epsilon */ { [] }
| ASSUMES full_lexpr SEMICOLON assumes { $2::$4 } | ASSUMES lexpr SEMICOLON assumes { $2::$4 }
| ASSUMES full_lexpr clause_kw { missing $loc($2) ";" $3 } | ASSUMES lexpr clause_kw { missing $loc($2) ";" $3 }
; ;
complete_or_disjoint: complete_or_disjoint:
...@@ -1358,7 +1283,7 @@ annotation: ...@@ -1358,7 +1283,7 @@ annotation:
(Not_well_formed (loc $sloc, (Not_well_formed (loc $sloc,
"Only one code annotation is allowed per comment")) "Only one code annotation is allowed per comment"))
} }
| full_identifier_or_typename { Aattribute_annot (loc $sloc, $1) } | identifier { Aattribute_annot (loc $sloc, $1) }
| BSGHOST { Aattribute_annot(loc(),"\\ghost") } | BSGHOST { Aattribute_annot(loc(),"\\ghost") }
; ;
...@@ -1447,7 +1372,7 @@ loop_annot_opt: ...@@ -1447,7 +1372,7 @@ loop_annot_opt:
; ;
loop_effects: loop_effects:
| LOOP ASSIGNS full_assigns SEMICOLON { $3 } | LOOP ASSIGNS assigns SEMICOLON { $3 }
; ;
loop_allocation: loop_allocation:
...@@ -1455,9 +1380,9 @@ loop_allocation: ...@@ -1455,9 +1380,9 @@ loop_allocation:
; ;
loop_invariant: loop_invariant:
| LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Assert $3 } | LOOP INVARIANT lexpr SEMICOLON { toplevel_pred Assert $3 }
| CHECK_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Check $3 } | CHECK_LOOP INVARIANT lexpr SEMICOLON { toplevel_pred Check $3 }
| ADMIT_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Admit $3 } | ADMIT_LOOP INVARIANT lexpr SEMICOLON { toplevel_pred Admit $3 }
; ;
loop_variant: loop_variant:
...@@ -1466,7 +1391,7 @@ loop_variant: ...@@ -1466,7 +1391,7 @@ loop_variant:
/* Grammar Extensibility for plugins */ /* Grammar Extensibility for plugins */
loop_grammar_extension: loop_grammar_extension:
| LOOP EXT_CODE_ANNOT grammar_extension SEMICOLON { | LOOP EXT_CODE_ANNOT extension_content SEMICOLON {
let open Cil_types in let open Cil_types in
let ext = $2 in let ext = $2 in
try try
...@@ -1487,7 +1412,7 @@ loop_grammar_extension: ...@@ -1487,7 +1412,7 @@ loop_grammar_extension:
; ;
loop_pragma: loop_pragma:
| LOOP PRAGMA any_identifier full_ne_lexpr_list SEMICOLON | LOOP PRAGMA any_identifier ne_lexpr_list SEMICOLON
{ if $3 = "UNROLL_LOOP" || $3 = "UNROLL" then { if $3 = "UNROLL_LOOP" || $3 = "UNROLL" then
(if $3 <> "UNROLL" then (if $3 <> "UNROLL" then
Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3; Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
...@@ -1523,19 +1448,19 @@ pragma_or_code_annotation: ...@@ -1523,19 +1448,19 @@ pragma_or_code_annotation:
; ;
code_annotation: code_annotation:
| ASSERT full_lexpr SEMICOLON | ASSERT lexpr SEMICOLON
{ fun bhvs -> AAssert (bhvs,toplevel_pred Assert $2) } { fun bhvs -> AAssert (bhvs,toplevel_pred Assert $2) }
| CHECK full_lexpr SEMICOLON | CHECK lexpr SEMICOLON
{ fun bhvs -> AAssert (bhvs,toplevel_pred Check $2) } { fun bhvs -> AAssert (bhvs,toplevel_pred Check $2) }
| ADMIT full_lexpr SEMICOLON | ADMIT lexpr SEMICOLON
{ fun bhvs -> AAssert (bhvs,toplevel_pred Admit $2) } { fun bhvs -> AAssert (bhvs,toplevel_pred Admit $2) }
| INVARIANT full_lexpr SEMICOLON | INVARIANT lexpr SEMICOLON
{ fun bhvs -> AInvariant (bhvs,false,toplevel_pred Assert $2) } { fun bhvs -> AInvariant (bhvs,false,toplevel_pred Assert $2) }
| CHECK_INVARIANT full_lexpr SEMICOLON | CHECK_INVARIANT lexpr SEMICOLON
{ fun bhvs -> AInvariant (bhvs,false,toplevel_pred Check $2) } { fun bhvs -> AInvariant (bhvs,false,toplevel_pred Check $2) }
| ADMIT_INVARIANT full_lexpr SEMICOLON | ADMIT_INVARIANT lexpr SEMICOLON
{ fun bhvs -> AInvariant (bhvs,false,toplevel_pred Admit $2) } { fun bhvs -> AInvariant (bhvs,false,toplevel_pred Admit $2) }
| EXT_CODE_ANNOT grammar_extension SEMICOLON | EXT_CODE_ANNOT extension_content SEMICOLON
{ fun bhvs -> { fun bhvs ->
let open Cil_types in let open Cil_types in
let ext = $1 in let ext = $1 in
...@@ -1559,7 +1484,7 @@ code_annotation: ...@@ -1559,7 +1484,7 @@ code_annotation:
; ;
slice_pragma: slice_pragma:
| SLICE PRAGMA any_identifier full_lexpr SEMICOLON | SLICE PRAGMA any_identifier lexpr SEMICOLON
{ if $3 = "expr" then SPexpr $4 { if $3 = "expr" then SPexpr $4
else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) } else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
| SLICE PRAGMA any_identifier SEMICOLON | SLICE PRAGMA any_identifier SEMICOLON
...@@ -1569,7 +1494,7 @@ slice_pragma: ...@@ -1569,7 +1494,7 @@ slice_pragma:
; ;
impact_pragma: impact_pragma:
| IMPACT PRAGMA any_identifier full_lexpr SEMICOLON | IMPACT PRAGMA any_identifier lexpr SEMICOLON
{ if $3 = "expr" then IPexpr $4 { if $3 = "expr" then IPexpr $4
else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) } else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) }
| IMPACT PRAGMA any_identifier SEMICOLON | IMPACT PRAGMA any_identifier SEMICOLON
...@@ -1585,9 +1510,9 @@ decl_list: ...@@ -1585,9 +1510,9 @@ decl_list:
; ;
decl: decl:
| GLOBAL INVARIANT any_identifier COLON full_lexpr SEMICOLON | GLOBAL INVARIANT any_identifier COLON lexpr SEMICOLON
{ LDinvariant ($3, $5) } { LDinvariant ($3, $5) }
| VOLATILE full_ne_zones volatile_opt SEMICOLON { LDvolatile ($2, $3) } | VOLATILE ne_zones volatile_opt SEMICOLON { LDvolatile ($2, $3) }
| type_annot {LDtype_annot $1} | type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1} | model_annot {LDmodel_annot $1}
| logic_def { $1 } | logic_def { $1 }
...@@ -1596,7 +1521,7 @@ decl: ...@@ -1596,7 +1521,7 @@ decl:
; ;
ext_decl: ext_decl:
| EXT_GLOBAL grammar_extension SEMICOLON { | EXT_GLOBAL extension_content SEMICOLON {
let processed = Logic_env.preprocess_extension $1 $2 in let processed = Logic_env.preprocess_extension $1 $2 in
Ext_lexpr($1, processed) Ext_lexpr($1, processed)
} }
...@@ -1638,8 +1563,8 @@ volatile_opt: ...@@ -1638,8 +1563,8 @@ volatile_opt:
; ;
type_annot: type_annot:
| TYPE INVARIANT any_identifier LPAR full_parameter RPAR EQUAL | TYPE INVARIANT any_identifier LPAR parameter RPAR EQUAL
full_lexpr SEMICOLON lexpr SEMICOLON
{ let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } } { let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } }
; ;
...@@ -1649,7 +1574,7 @@ opt_semicolon: ...@@ -1649,7 +1574,7 @@ opt_semicolon:
; ;
model_annot: model_annot:
| MODEL type_spec LBRACE full_parameter opt_semicolon RBRACE SEMICOLON | MODEL type_spec(typename) LBRACE parameter opt_semicolon RBRACE SEMICOLON
{ let typ,name = $4 in { let typ,name = $4 in
{ model_for_type = $2; model_name = name; model_type = typ; } { model_for_type = $2; model_name = name; model_type = typ; }
} }
...@@ -1683,17 +1608,17 @@ opt_parameters: ...@@ -1683,17 +1608,17 @@ opt_parameters:
; ;
parameters: parameters:
| LPAR full_parameters RPAR { $2 } | LPAR ne_parameters RPAR { $2 }
; ;
logic_def: logic_def:
/* logic function definition */ /* logic function definition */
| LOGIC full_logic_rt_type poly_id opt_parameters EQUAL full_lexpr SEMICOLON | LOGIC logic_rt_type poly_id opt_parameters EQUAL lexpr SEMICOLON
{ let (id, labels, tvars) = $3 in { let (id, labels, tvars) = $3 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDlogic_def (id, labels, tvars, $2, $4, $6) } LDlogic_def (id, labels, tvars, $2, $4, $6) }
/* predicate definition */ /* predicate definition */
| PREDICATE poly_id opt_parameters EQUAL full_lexpr SEMICOLON | PREDICATE poly_id opt_parameters EQUAL lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in { let (id,labels,tvars) = $2 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDpredicate_def (id, labels, tvars, $3, $5) } LDpredicate_def (id, labels, tvars, $3, $5) }
...@@ -1702,15 +1627,15 @@ logic_def: ...@@ -1702,15 +1627,15 @@ logic_def:
{ let (id,labels,tvars) = $2 in { let (id,labels,tvars) = $2 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDinductive_def(id, labels, tvars, $3, $5) } LDinductive_def(id, labels, tvars, $3, $5) }
| LEMMA poly_id COLON full_lexpr SEMICOLON | LEMMA poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in { let (id,labels,tvars) = $2 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Assert $4) } LDlemma (id, labels, tvars, toplevel_pred Assert $4) }
| CHECK_LEMMA poly_id COLON full_lexpr SEMICOLON | CHECK_LEMMA poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in { let (id,labels,tvars) = $2 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Check $4) } LDlemma (id, labels, tvars, toplevel_pred Check $4) }
| ADMIT_LEMMA poly_id COLON full_lexpr SEMICOLON | ADMIT_LEMMA poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in { let (id,labels,tvars) = $2 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Admit $4) } LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
...@@ -1725,7 +1650,7 @@ logic_def: ...@@ -1725,7 +1650,7 @@ logic_def:
deprecated_logic_decl: deprecated_logic_decl:
/* OBSOLETE: logic function declaration */ /* OBSOLETE: logic function declaration */
| LOGIC full_logic_rt_type poly_id opt_parameters SEMICOLON | LOGIC logic_rt_type poly_id opt_parameters SEMICOLON
{ let (id, labels, tvars) = $3 in { let (id, labels, tvars) = $3 in
let source = pos $symbolstartpos in let source = pos $symbolstartpos in
exit_type_variables_scope (); exit_type_variables_scope ();
...@@ -1748,7 +1673,7 @@ deprecated_logic_decl: ...@@ -1748,7 +1673,7 @@ deprecated_logic_decl:
LDtype(id,tvars,None) LDtype(id,tvars,None)
} }
/* OBSOLETE: axiom */ /* OBSOLETE: axiom */
| AXIOM poly_id COLON full_lexpr SEMICOLON | AXIOM poly_id COLON lexpr SEMICOLON
{ let (id,_,_) = $2 in { let (id,_,_) = $2 in
raise raise
(Not_well_formed (Not_well_formed
...@@ -1767,7 +1692,7 @@ logic_decls: ...@@ -1767,7 +1692,7 @@ logic_decls:
logic_decl: logic_decl:
| logic_def { $1 } | logic_def { $1 }
/* logic function declaration */ /* logic function declaration */
| LOGIC full_logic_rt_type poly_id opt_parameters reads_clause SEMICOLON | LOGIC logic_rt_type poly_id opt_parameters reads_clause SEMICOLON
{ let (id, labels, tvars) = $3 in { let (id, labels, tvars) = $3 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDlogic_reads (id, labels, tvars, $2, $4, $5) } LDlogic_reads (id, labels, tvars, $2, $4, $5) }
...@@ -1783,7 +1708,7 @@ logic_decl: ...@@ -1783,7 +1708,7 @@ logic_decl:
exit_type_variables_scope (); exit_type_variables_scope ();
LDtype(id,tvars,None) } LDtype(id,tvars,None) }
/* axiom */ /* axiom */
| AXIOM poly_id COLON full_lexpr SEMICOLON | AXIOM poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in { let (id,labels,tvars) = $2 in
exit_type_variables_scope (); exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Admit $4) } LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
...@@ -1796,12 +1721,12 @@ logic_decl_loc: ...@@ -1796,12 +1721,12 @@ logic_decl_loc:
reads_clause: reads_clause:
| /* epsilon */ { None } | /* epsilon */ { None }
| READS full_zones { Some $2 } | READS zones { Some $2 }
; ;
typedef: typedef:
| ne_datacons_list { TDsum $1 } | ne_datacons_list { TDsum $1 }
| full_logic_type { TDsyn $1 } | logic_type { TDsyn $1 }
; ;
datacons_list: datacons_list:
...@@ -1820,13 +1745,13 @@ datacons: ...@@ -1820,13 +1745,13 @@ datacons:
; ;
ne_type_list: ne_type_list:
| full_logic_type { [$1] } | logic_type { [$1] }
| full_logic_type COMMA ne_type_list { $1::$3 } | logic_type COMMA ne_type_list { $1::$3 }
indcases: indcases:
| /* epsilon */ | /* epsilon */
{ [] } { [] }
| CASE poly_id COLON full_lexpr SEMICOLON indcases | CASE poly_id COLON lexpr SEMICOLON indcases
{ let (id,labels,tvars) = $2 in { let (id,labels,tvars) = $2 in
exit_type_variables_scope (); exit_type_variables_scope ();
(id,labels,tvars,$4)::$6 } (id,labels,tvars,$4)::$6 }
...@@ -1883,19 +1808,20 @@ behavior_name: ...@@ -1883,19 +1808,20 @@ behavior_name:
; ;
any_identifier: any_identifier:
| identifier_or_typename { $1 } | identifier { $1 }
| is_acsl_typename { $1 }
| TYPENAME { $1 }
| keyword { $1 } | keyword { $1 }
; ;
identifier_or_typename: /* allowed as C field names */ identifier_or_typename:
| is_acsl_typename { $1 }
| TYPENAME { $1 } /* followed by the same list than 'identifier' */ | TYPENAME { $1 } /* followed by the same list than 'identifier' */
| IDENTIFIER { $1 } | full_identifier { $1 }
/* token list used inside acsl clauses: */
| BEHAVIORS { "behaviors" }
| LABEL { "label" } identifier_or_typename_full: /* allowed as C field names */
| READS { "reads" } | is_acsl_typename { $1 }
| WRITES { "writes" } | identifier_or_typename { $1 }
; ;
identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */ identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment