Skip to content
Snippets Groups Projects
Commit 8edd3dc6 authored by Thibault Martin's avatar Thibault Martin
Browse files

[lint] Cleaning c parser

parent 7c6b74ae
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_internals/parsing/cparser.mly
+ 901
− 945
View file @ 8edd3dc6
...@@ -78,7 +78,7 @@ exception NoProto ...@@ -78,7 +78,7 @@ exception NoProto
(* Go through all the parameter names and mark them as identifiers *) (* Go through all the parameter names and mark them as identifiers *)
let rec findProto = function let rec findProto = function
PROTO (d, args, _,_) when isJUSTBASE d -> PROTO (d, args, _,_) when isJUSTBASE d ->
List.iter (fun (_, (an, _, _, _)) -> !Lexerhack.add_identifier an) args List.iter (fun (_, (an, _, _, _)) -> !Lexerhack.add_identifier an) args
| PROTO (d, _,_, _) -> findProto d | PROTO (d, _,_, _) -> findProto d
| PARENTYPE (_, d, _) -> findProto d | PARENTYPE (_, d, _) -> findProto d
| PTR (_, d) -> findProto d | PTR (_, d) -> findProto d
...@@ -102,21 +102,19 @@ let announceFunctionName ((n, decl, _, loc):name) = ...@@ -102,21 +102,19 @@ let announceFunctionName ((n, decl, _, loc):name) =
currentFunctionName := n currentFunctionName := n
let check_funspec_abrupt_clauses fname spec = let check_funspec_abrupt_clauses fname spec =
List.iter List.iter (fun bhv ->
(fun bhv -> List.iter (function
List.iter | (Cil_types.Normal | Cil_types.Exits),_ -> ()
(function | (Cil_types.Breaks | Cil_types.Continues | Cil_types.Returns),
| (Cil_types.Normal | Cil_types.Exits),_ -> () { Logic_ptree.tp_statement = { lexpr_loc = loc}} ->
| (Cil_types.Breaks | Cil_types.Continues | Cil_types.Returns), Errorloc.parse_error ~loc
{ Logic_ptree.tp_statement = { lexpr_loc = loc}} -> "Specification of function %s can only contain ensures or \
Errorloc.parse_error ~loc exits post-conditions" fname)
"Specification of function %s can only contain ensures or \ bhv.Logic_ptree.b_post_cond)
exits post-conditions" fname)
bhv.Logic_ptree.b_post_cond)
spec.Logic_ptree.spec_behavior spec.Logic_ptree.spec_behavior
let applyPointer (ptspecs: attribute list list) (dt: decl_type) let applyPointer (ptspecs: attribute list list) (dt: decl_type)
: decl_type = : decl_type =
(* Outer specification first *) (* Outer specification first *)
let rec loop = function let rec loop = function
[] -> dt [] -> dt
...@@ -135,33 +133,33 @@ let doDeclaration logic_spec (loc: cabsloc) (specs: spec_elem list) (nl: init_na ...@@ -135,33 +133,33 @@ let doDeclaration logic_spec (loc: cabsloc) (specs: spec_elem list) (nl: init_na
if isTypedef specs then begin if isTypedef specs then begin
TYPEDEF ((specs, List.map (fun (n, _) -> n) nl), loc) TYPEDEF ((specs, List.map (fun (n, _) -> n) nl), loc)
end else end else
if nl = [] then if nl = [] then
ONLYTYPEDEF (specs, loc) ONLYTYPEDEF (specs, loc)
else begin else begin
!Lexerhack.push_context (); !Lexerhack.push_context ();
List.iter List.iter
(fun ((_,t,_,_),_) -> (fun ((_,t,_,_),_) ->
try findProto t with NoProto -> ()) try findProto t with NoProto -> ())
nl; nl;
let logic_spec = let logic_spec =
match logic_spec with match logic_spec with
| None -> None | None -> None
| Some (loc, _ as ls) -> begin | Some (loc, _ as ls) -> begin
Option.map Option.map
(fun (loc', spec) -> (fun (loc', spec) ->
let name = let name =
match nl with match nl with
| [ (n,_,_,_),_ ] -> n | [ (n,_,_,_),_ ] -> n
| _ -> "unknown function" | _ -> "unknown function"
in in
check_funspec_abrupt_clauses name spec; check_funspec_abrupt_clauses name spec;
(spec, (loc, loc'))) (spec, (loc, loc')))
(Logic_lexer.spec ls) (Logic_lexer.spec ls)
end end
in in
!Lexerhack.pop_context (); !Lexerhack.pop_context ();
DECDEF (logic_spec, (specs, nl), loc) DECDEF (logic_spec, (specs, nl), loc)
end end
let in_ghost = let in_ghost =
let ghost_me = object let ghost_me = object
...@@ -177,10 +175,10 @@ let in_ghost = ...@@ -177,10 +175,10 @@ let in_ghost =
let ghost_global = ref false let ghost_global = ref false
let doFunctionDef spec (loc: cabsloc) let doFunctionDef spec (loc: cabsloc)
(lend: cabsloc) (lend: cabsloc)
(specs: spec_elem list) (specs: spec_elem list)
(n: name) (n: name)
(b: block) : definition = (b: block) : definition =
let fname = (specs, n) in let fname = (specs, n) in
let name = match n with (n,_,_,_) -> n in let name = match n with (n,_,_,_) -> n in
Option.iter (fun (spec, _) -> check_funspec_abrupt_clauses name spec) spec; Option.iter (fun (spec, _) -> check_funspec_abrupt_clauses name spec) spec;
...@@ -194,12 +192,12 @@ let doOldParDecl floc (names: string list) ...@@ -194,12 +192,12 @@ let doOldParDecl floc (names: string list)
let rec loopGroups = function let rec loopGroups = function
| [] -> ([SpecType Tint], (n, JUSTBASE, [], floc)) | [] -> ([SpecType Tint], (n, JUSTBASE, [], floc))
| (specs, names) :: restgroups -> | (specs, names) :: restgroups ->
let rec loopNames = function let rec loopNames = function
| [] -> loopGroups restgroups | [] -> loopGroups restgroups
| ((n',_, _, _) as sn) :: _ when n' = n -> (specs, sn) | ((n',_, _, _) as sn) :: _ when n' = n -> (specs, sn)
| _ :: restnames -> loopNames restnames | _ :: restnames -> loopNames restnames
in in
loopNames names loopNames names
in in
loopGroups pardefs loopGroups pardefs
in in
...@@ -208,7 +206,7 @@ let doOldParDecl floc (names: string list) ...@@ -208,7 +206,7 @@ let doOldParDecl floc (names: string list)
let int64_to_char ~loc value = let int64_to_char ~loc value =
if (Int64.compare value (Int64.of_int 255) > 0) || if (Int64.compare value (Int64.of_int 255) > 0) ||
(Int64.compare value Int64.zero < 0) then (Int64.compare value Int64.zero < 0) then
Errorloc.parse_error ~loc "integral literal 0x%Lx too big" value Errorloc.parse_error ~loc "integral literal 0x%Lx too big" value
else else
Char.chr (Int64.to_int value) Char.chr (Int64.to_int value)
...@@ -259,15 +257,15 @@ let transformOffsetOf (speclist, dtype) member = ...@@ -259,15 +257,15 @@ let transformOffsetOf (speclist, dtype) member =
let mk_expr e = { expr_loc = member.expr_loc; expr_node = e } in let mk_expr e = { expr_loc = member.expr_loc; expr_node = e } in
let rec addPointer = function let rec addPointer = function
| JUSTBASE -> | JUSTBASE ->
PTR([], JUSTBASE) PTR([], JUSTBASE)
| PARENTYPE (attrs1, dtype, attrs2) -> | PARENTYPE (attrs1, dtype, attrs2) ->
PARENTYPE (attrs1, addPointer dtype, attrs2) PARENTYPE (attrs1, addPointer dtype, attrs2)
| ARRAY (dtype, attrs, expr) -> | ARRAY (dtype, attrs, expr) ->
ARRAY (addPointer dtype, attrs, expr) ARRAY (addPointer dtype, attrs, expr)
| PTR (attrs, dtype) -> | PTR (attrs, dtype) ->
PTR (attrs, addPointer dtype) PTR (attrs, addPointer dtype)
| PROTO (dtype, names, gnames, variadic) -> | PROTO (dtype, names, gnames, variadic) ->
PROTO (addPointer dtype, names, gnames,variadic) PROTO (addPointer dtype, names, gnames,variadic)
in in
let nullType = (speclist, addPointer dtype) in let nullType = (speclist, addPointer dtype) in
let nullExpr = mk_expr (CONSTANT (CONST_INT "0")) in let nullExpr = mk_expr (CONSTANT (CONST_INT "0")) in
...@@ -305,15 +303,15 @@ let in_block sloc l = ...@@ -305,15 +303,15 @@ let in_block sloc l =
Errorloc.parse_error ~loc "empty list of statement, should not happen" Errorloc.parse_error ~loc "empty list of statement, should not happen"
| [s] -> s | [s] -> s
| _::_ -> | _::_ ->
no_ghost_stmt (BLOCK ({ blabels = []; battrs = []; bstmts = l}, no_ghost_stmt (BLOCK ({ blabels = []; battrs = []; bstmts = l},
get_statementloc (List.hd l), get_statementloc (List.hd l),
get_statementloc (Extlib.last l))) get_statementloc (Extlib.last l)))
let in_ghost_block ?(battrs=[]) l = let in_ghost_block ?(battrs=[]) l =
let l = in_ghost l in let l = in_ghost l in
ghost_stmt (BLOCK ({ blabels = []; battrs ; bstmts = l}, ghost_stmt (BLOCK ({ blabels = []; battrs ; bstmts = l},
get_statementloc (List.hd l), get_statementloc (List.hd l),
get_statementloc (Extlib.last l))) get_statementloc (Extlib.last l)))
%} %}
...@@ -453,13 +451,13 @@ let in_ghost_block ?(battrs=[]) l = ...@@ -453,13 +451,13 @@ let in_ghost_block ?(battrs=[]) l =
interpret: file { $1 } interpret: file { $1 }
file: globals EOF {$1} file: globals EOF {$1}
globals: globals:
/* empty */ { [] } | /* empty */ { [] }
| global globals { (false,$1) :: $2 } | global globals { (false,$1) :: $2 }
| ghost_glob_begin ghost_globals globals { $2 @ $3 } | ghost_glob_begin ghost_globals globals { $2 @ $3 }
| SEMICOLON globals { $2 } | SEMICOLON globals { $2 }
; ;
ghost_glob_begin: ghost_glob_begin:
...@@ -468,431 +466,411 @@ ghost_glob_begin: ...@@ -468,431 +466,411 @@ ghost_glob_begin:
/* Rules for global ghosts: TODO keep the ghost status! */ /* Rules for global ghosts: TODO keep the ghost status! */
ghost_globals: ghost_globals:
| declaration ghost_globals { (true,$1)::$2 } | declaration ghost_globals { (true,$1)::$2 }
| function_def ghost_globals { (true,$1)::$2 } | function_def ghost_globals { (true,$1)::$2 }
| RGHOST { ghost_global:=false; [] } | RGHOST { ghost_global:=false; [] }
; ;
/*** Global Definition ***/ /*** Global Definition ***/
global: global:
| DECL { GLOBANNOT $1 } | DECL { GLOBANNOT $1 }
| declaration { $1 } | declaration { $1 }
| function_def { $1 } | function_def { $1 }
/*(* Some C header files are shared with the C++ compiler and have linkage /*(* Some C header files are shared with the C++ compiler and have linkage
* specification *)*/ * specification *)*/
| EXTERN string_constant declaration | EXTERN string_constant declaration
{ LINKAGE (fst $2, (*handleLoc*) (snd $2), [ $3 ]) } { LINKAGE (fst $2, (*handleLoc*) (snd $2), [ $3 ]) }
| EXTERN string_constant LBRACE globals RBRACE | EXTERN string_constant LBRACE globals RBRACE {
{ LINKAGE ( LINKAGE (
fst $2, (*handleLoc*) (snd $2), fst $2, (*handleLoc*) (snd $2),
List.map List.map
(fun (x,y) -> (fun (x,y) ->
if x then if x then
let loc = Cabshelper.get_definitionloc y in let loc = Cabshelper.get_definitionloc y in
Errorloc.parse_error ~loc Errorloc.parse_error ~loc
"invalid ghost in extern linkage specification" "invalid ghost in extern linkage specification"
else y) else y)
$4) $4
} )
}
| ASM LPAREN string_constant RPAREN SEMICOLON | ASM LPAREN string_constant RPAREN SEMICOLON
{ GLOBASM (fst $3, (*handleLoc*) $1) } { GLOBASM (fst $3, (*handleLoc*) $1) }
| pragma { $1 } | pragma { $1 }
/* (* Old-style function prototype. This should be somewhere else, like in /* (* Old-style function prototype. This should be somewhere else, like in
* "declaration". For now we keep it at global scope only because in local * "declaration". For now we keep it at global scope only because in local
* scope it looks too much like a function call *) */ * scope it looks too much like a function call *) */
| f=IDENT LPAREN prms=old_parameter_list_ne RPAREN | f=IDENT LPAREN prms=old_parameter_list_ne RPAREN decls=old_pardef_list SEMICOLON {
decls=old_pardef_list SEMICOLON let dloc = Cil_datatype.Location.of_lexing_loc $loc in
{ let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in
let dloc = Cil_datatype.Location.of_lexing_loc $loc in (* Convert pardecl to new style *)
let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in let pardecl, isva = doOldParDecl floc prms decls in
(* Convert pardecl to new style *) (* Make the function declarator *)
let pardecl, isva = doOldParDecl floc prms decls in doDeclaration None dloc []
(* Make the function declarator *) [((f, PROTO(JUSTBASE, pardecl,[],isva),
doDeclaration None dloc [] ["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)]
[((f, PROTO(JUSTBASE, pardecl,[],isva), }
["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)]
}
| f=IDENT LPAREN RPAREN SEMICOLON { | f=IDENT LPAREN RPAREN SEMICOLON {
let dloc = Cil_datatype.Location.of_lexing_loc $loc in let dloc = Cil_datatype.Location.of_lexing_loc $loc in
let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in
doDeclaration None dloc [] doDeclaration None dloc []
[((f, PROTO(JUSTBASE,[],[],false), [((f, PROTO(JUSTBASE,[],[],false),
["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)] ["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)]
} }
; ;
id_or_typename_as_id: id_or_typename_as_id:
IDENT { $1 } | IDENT { $1 }
| NAMED_TYPE { $1 } | NAMED_TYPE { $1 }
; ;
id_or_typename: id_or_typename: id_or_typename_as_id { $1 }
id_or_typename_as_id { $1 }
;
maybecomma: maybecomma:
/* empty */ { () } | /* empty */ { () }
| COMMA { () } | COMMA { () }
; ;
/* *** Expressions *** */ /* *** Expressions *** */
primary_expression: /*(* 6.5.1. *)*/ primary_expression: /*(* 6.5.1. *)*/
| IDENT { make_expr $sloc (VARIABLE $1) } | IDENT { make_expr $sloc (VARIABLE $1) }
| constant { | constant {
let (v,expr_loc) = $1 in { expr_loc; expr_node = CONSTANT v } } let (v,expr_loc) = $1 in
| paren_comma_expression { expr_loc; expr_node = CONSTANT v }
{ make_expr $sloc (PAREN (smooth_expression $1)) } }
| LPAREN block RPAREN { make_expr $sloc (GNU_BODY (fst3 $2)) } | paren_comma_expression { make_expr $sloc (PAREN (smooth_expression $1)) }
| generic_selection { make_expr $sloc (GENERIC $1) } | LPAREN block RPAREN { make_expr $sloc (GNU_BODY (fst3 $2)) }
| generic_selection { make_expr $sloc (GENERIC $1) }
; ;
postfix_expression: /*(* 6.5.2 *)*/ postfix_expression: /*(* 6.5.2 *)*/
| primary_expression { $1 } | primary_expression { $1 }
| postfix_expression bracket_comma_expression | postfix_expression bracket_comma_expression
{ make_expr $sloc (INDEX ($1, smooth_expression $2))} { make_expr $sloc (INDEX ($1, smooth_expression $2))}
| postfix_expression LPAREN arguments RPAREN ghost_arguments_opt | postfix_expression LPAREN arguments RPAREN ghost_arguments_opt
{ make_expr $sloc (CALL ($1, $3, $5))} { make_expr $sloc (CALL ($1, $3, $5))}
| BUILTIN_VA_ARG LPAREN expression COMMA type_name RPAREN | BUILTIN_VA_ARG LPAREN expression COMMA type_name RPAREN {
{ let b, d = $5 in let b, d = $5 in
let loc = Cil_datatype.Location.of_lexing_loc $loc($5) in let loc = Cil_datatype.Location.of_lexing_loc $loc($5) in
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
make_expr $sloc make_expr $sloc
(CALL (CALL
({ expr_loc = loc_f; ({ expr_loc = loc_f;
expr_node = VARIABLE "__builtin_va_arg"}, expr_node = VARIABLE "__builtin_va_arg"},
[$3; { expr_loc = loc; [$3; { expr_loc = loc;
expr_node = TYPE_SIZEOF (b, d)}],[])) expr_node = TYPE_SIZEOF (b, d)}],[]))
} }
| BUILTIN_TYPES_COMPAT LPAREN type_name COMMA type_name RPAREN | BUILTIN_TYPES_COMPAT LPAREN type_name COMMA type_name RPAREN {
{ let b1,d1 = $3 in let b1,d1 = $3 in
let b2,d2 = $5 in let b2,d2 = $5 in
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
let loc1 = Cil_datatype.Location.of_lexing_loc $loc($3) in let loc1 = Cil_datatype.Location.of_lexing_loc $loc($3) in
let loc2 = Cil_datatype.Location.of_lexing_loc $loc($5) in let loc2 = Cil_datatype.Location.of_lexing_loc $loc($5) in
make_expr $sloc make_expr $sloc
(CALL (CALL
({expr_loc = loc_f; ({expr_loc = loc_f;
expr_node = VARIABLE "__builtin_types_compatible_p"}, expr_node = VARIABLE "__builtin_types_compatible_p"},
[ { expr_loc = loc1; expr_node = TYPE_SIZEOF(b1,d1)}; [ { expr_loc = loc1; expr_node = TYPE_SIZEOF(b1,d1)};
{ expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[])) { expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[]))
} }
| BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN | BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN {
{ let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in let arg = transformOffsetOf $3 $5 in
let arg = transformOffsetOf $3 $5 in let builtin = { expr_loc = loc_f;
let builtin = { expr_loc = loc_f; expr_node = VARIABLE "__builtin_offsetof" }
expr_node = VARIABLE "__builtin_offsetof" } in
in make_expr $sloc (CALL (builtin, [ arg ], []))
make_expr $sloc (CALL (builtin, [ arg ], [])) }
} | postfix_expression DOT id_or_typename { make_expr $sloc (MEMBEROF ($1, $3)) }
| postfix_expression DOT id_or_typename { make_expr $sloc (MEMBEROF ($1, $3))} | postfix_expression ARROW id_or_typename
| postfix_expression ARROW id_or_typename { make_expr $sloc (MEMBEROFPTR ($1, $3)) } { make_expr $sloc (MEMBEROFPTR ($1, $3)) }
| postfix_expression PLUS_PLUS { make_expr $sloc (UNARY (POSINCR, $1)) } | postfix_expression PLUS_PLUS { make_expr $sloc (UNARY (POSINCR, $1)) }
| postfix_expression MINUS_MINUS { make_expr $sloc (UNARY (POSDECR, $1)) } | postfix_expression MINUS_MINUS { make_expr $sloc (UNARY (POSDECR, $1)) }
/* (* We handle GCC constructor expressions *) */ /* (* We handle GCC constructor expressions *) */
| LPAREN type_name RPAREN LBRACE initializer_list_opt RBRACE | LPAREN type_name RPAREN LBRACE initializer_list_opt RBRACE
{ make_expr $sloc (CAST($2, COMPOUND_INIT $5)) } { make_expr $sloc (CAST($2, COMPOUND_INIT $5)) }
; ;
offsetof_member_designator: /* GCC extension for __builtin_offsetof */ offsetof_member_designator: /* GCC extension for __builtin_offsetof */
| id_or_typename { make_expr $sloc (VARIABLE $1) } | id_or_typename { make_expr $sloc (VARIABLE $1) }
| offsetof_member_designator DOT IDENT | offsetof_member_designator DOT IDENT { make_expr $sloc (MEMBEROF ($1, $3)) }
{ make_expr $sloc (MEMBEROF ($1, $3)) } | offsetof_member_designator bracket_comma_expression
| offsetof_member_designator bracket_comma_expression { make_expr $sloc (INDEX ($1, smooth_expression $2)) }
{ make_expr $sloc (INDEX ($1, smooth_expression $2)) }
; ;
unary_expression: /*(* 6.5.3 *)*/ unary_expression: /*(* 6.5.3 *)*/
| postfix_expression | postfix_expression { $1 }
{ $1 } | PLUS_PLUS unary_expression { make_expr $sloc (UNARY (PREINCR, $2)) }
| PLUS_PLUS unary_expression | MINUS_MINUS unary_expression { make_expr $sloc (UNARY (PREDECR, $2)) }
{ make_expr $sloc (UNARY (PREINCR, $2))} | SIZEOF unary_expression { make_expr $sloc (EXPR_SIZEOF $2) }
| MINUS_MINUS unary_expression | SIZEOF LPAREN type_name RPAREN
{ make_expr $sloc (UNARY (PREDECR, $2))} { let b, d = $3 in make_expr $sloc (TYPE_SIZEOF (b, d)) }
| SIZEOF unary_expression | ALIGNOF unary_expression { make_expr $sloc (EXPR_ALIGNOF $2) }
{ make_expr $sloc (EXPR_SIZEOF $2)} | ALIGNOF LPAREN type_name RPAREN
| SIZEOF LPAREN type_name RPAREN {let b, d = $3 in make_expr $sloc (TYPE_ALIGNOF (b, d)) }
{ let b, d = $3 in make_expr $sloc (TYPE_SIZEOF (b, d)) } | PLUS cast_expression { make_expr $sloc (UNARY (PLUS, $2)) }
| ALIGNOF unary_expression | MINUS cast_expression { make_expr $sloc (UNARY (MINUS, $2)) }
{ make_expr $sloc (EXPR_ALIGNOF $2) } | STAR cast_expression { make_expr $sloc (UNARY (MEMOF, $2)) }
| ALIGNOF LPAREN type_name RPAREN | AND cast_expression { make_expr $sloc (UNARY (ADDROF, $2)) }
{let b, d = $3 in make_expr $sloc (TYPE_ALIGNOF (b, d)) } | EXCLAM cast_expression { make_expr $sloc (UNARY (NOT, $2)) }
| PLUS cast_expression | TILDE cast_expression { make_expr $sloc (UNARY (BNOT, $2)) }
{ make_expr $sloc (UNARY (PLUS, $2)) }
| MINUS cast_expression
{ make_expr $sloc (UNARY (MINUS, $2)) }
| STAR cast_expression
{ make_expr $sloc (UNARY (MEMOF, $2)) }
| AND cast_expression
{ make_expr $sloc (UNARY (ADDROF, $2))}
| EXCLAM cast_expression
{ make_expr $sloc (UNARY (NOT, $2)) }
| TILDE cast_expression
{ make_expr $sloc (UNARY (BNOT, $2)) }
/* (* GCC allows to take address of a label (see COMPGOTO statement) *) */ /* (* GCC allows to take address of a label (see COMPGOTO statement) *) */
| AND_AND id_or_typename_as_id { make_expr $sloc (LABELADDR $2) } | AND_AND id_or_typename_as_id { make_expr $sloc (LABELADDR $2) }
; ;
cast_expression: /*(* 6.5.4 *)*/ cast_expression: /*(* 6.5.4 *)*/
| unary_expression { $1 } | unary_expression { $1 }
| LPAREN type_name RPAREN cast_expression | LPAREN type_name RPAREN cast_expression
{ make_expr $sloc (CAST($2, SINGLE_INIT $4)) } { make_expr $sloc (CAST($2, SINGLE_INIT $4)) }
; ;
multiplicative_expression: /*(* 6.5.5 *)*/ multiplicative_expression: /*(* 6.5.5 *)*/
| cast_expression { $1 } | cast_expression { $1 }
| multiplicative_expression STAR cast_expression | multiplicative_expression STAR cast_expression
{ make_expr $sloc (BINARY(MUL, $1, $3)) } { make_expr $sloc (BINARY(MUL, $1, $3)) }
| multiplicative_expression SLASH cast_expression | multiplicative_expression SLASH cast_expression
{ make_expr $sloc (BINARY(DIV, $1, $3)) } { make_expr $sloc (BINARY(DIV, $1, $3)) }
| multiplicative_expression PERCENT cast_expression | multiplicative_expression PERCENT cast_expression
{ make_expr $sloc (BINARY(MOD, $1, $3)) } { make_expr $sloc (BINARY(MOD, $1, $3)) }
; ;
additive_expression: /*(* 6.5.6 *)*/ additive_expression: /*(* 6.5.6 *)*/
| multiplicative_expression { $1 } | multiplicative_expression { $1 }
| additive_expression PLUS multiplicative_expression | additive_expression PLUS multiplicative_expression
{ make_expr $sloc (BINARY(ADD, $1, $3)) } { make_expr $sloc (BINARY(ADD, $1, $3)) }
| additive_expression MINUS multiplicative_expression | additive_expression MINUS multiplicative_expression
{ make_expr $sloc (BINARY(SUB, $1, $3)) } { make_expr $sloc (BINARY(SUB, $1, $3)) }
; ;
shift_expression: /*(* 6.5.7 *)*/ shift_expression: /*(* 6.5.7 *)*/
| additive_expression { $1 } | additive_expression { $1 }
| shift_expression INF_INF additive_expression | shift_expression INF_INF additive_expression
{ make_expr $sloc (BINARY(SHL, $1, $3)) } { make_expr $sloc (BINARY(SHL, $1, $3)) }
| shift_expression SUP_SUP additive_expression | shift_expression SUP_SUP additive_expression
{ make_expr $sloc (BINARY(SHR, $1, $3)) } { make_expr $sloc (BINARY(SHR, $1, $3)) }
; ;
relational_expression: /*(* 6.5.8 *)*/ relational_expression: /*(* 6.5.8 *)*/
| shift_expression { $1 } | shift_expression { $1 }
| relational_expression INF shift_expression | relational_expression INF shift_expression
{ make_expr $sloc (BINARY(LT, $1, $3)) } { make_expr $sloc (BINARY(LT, $1, $3)) }
| relational_expression SUP shift_expression | relational_expression SUP shift_expression
{ make_expr $sloc (BINARY(GT, $1, $3)) } { make_expr $sloc (BINARY(GT, $1, $3)) }
| relational_expression INF_EQ shift_expression | relational_expression INF_EQ shift_expression
{ make_expr $sloc (BINARY(LE, $1, $3)) } { make_expr $sloc (BINARY(LE, $1, $3)) }
| relational_expression SUP_EQ shift_expression | relational_expression SUP_EQ shift_expression
{ make_expr $sloc (BINARY(GE, $1, $3)) } { make_expr $sloc (BINARY(GE, $1, $3)) }
; ;
equality_expression: /*(* 6.5.9 *)*/ equality_expression: /*(* 6.5.9 *)*/
| relational_expression { $1 } | relational_expression { $1 }
| equality_expression EQ_EQ relational_expression | equality_expression EQ_EQ relational_expression
{ make_expr $sloc (BINARY(EQ, $1, $3)) } { make_expr $sloc (BINARY(EQ, $1, $3)) }
| equality_expression EXCLAM_EQ relational_expression | equality_expression EXCLAM_EQ relational_expression
{ make_expr $sloc (BINARY(NE, $1, $3)) } { make_expr $sloc (BINARY(NE, $1, $3)) }
; ;
bitwise_and_expression: /*(* 6.5.10 *)*/ bitwise_and_expression: /*(* 6.5.10 *)*/
| equality_expression { $1 } | equality_expression { $1 }
| bitwise_and_expression AND equality_expression | bitwise_and_expression AND equality_expression
{ make_expr $sloc (BINARY(BAND, $1, $3)) } { make_expr $sloc (BINARY(BAND, $1, $3)) }
; ;
bitwise_xor_expression: /*(* 6.5.11 *)*/ bitwise_xor_expression: /*(* 6.5.11 *)*/
| bitwise_and_expression { $1 } | bitwise_and_expression { $1 }
| bitwise_xor_expression CIRC bitwise_and_expression | bitwise_xor_expression CIRC bitwise_and_expression
{ make_expr $sloc (BINARY(XOR, $1, $3)) } { make_expr $sloc (BINARY(XOR, $1, $3)) }
; ;
bitwise_or_expression: /*(* 6.5.12 *)*/ bitwise_or_expression: /*(* 6.5.12 *)*/
| bitwise_xor_expression { $1 } | bitwise_xor_expression { $1 }
| bitwise_or_expression PIPE bitwise_xor_expression | bitwise_or_expression PIPE bitwise_xor_expression
{ make_expr $sloc (BINARY(BOR, $1, $3)) } { make_expr $sloc (BINARY(BOR, $1, $3)) }
; ;
logical_and_expression: /*(* 6.5.13 *)*/ logical_and_expression: /*(* 6.5.13 *)*/
| bitwise_or_expression { $1 } | bitwise_or_expression { $1 }
| logical_and_expression AND_AND bitwise_or_expression | logical_and_expression AND_AND bitwise_or_expression
{ make_expr $sloc (BINARY(AND, $1, $3)) } { make_expr $sloc (BINARY(AND, $1, $3)) }
; ;
logical_or_expression: /*(* 6.5.14 *)*/ logical_or_expression: /*(* 6.5.14 *)*/
| logical_and_expression { $1 } | logical_and_expression { $1 }
| logical_or_expression PIPE_PIPE logical_and_expression | logical_or_expression PIPE_PIPE logical_and_expression
{ make_expr $sloc (BINARY(OR, $1, $3)) } { make_expr $sloc (BINARY(OR, $1, $3)) }
; ;
conditional_expression: /*(* 6.5.15 *)*/ conditional_expression: /*(* 6.5.15 *)*/
| logical_or_expression { $1 } | logical_or_expression { $1 }
| logical_or_expression QUEST opt_expression COLON conditional_expression | logical_or_expression QUEST opt_expression COLON conditional_expression
{ make_expr $sloc (QUESTION ($1, $3, $5)) } { make_expr $sloc (QUESTION ($1, $3, $5)) }
; ;
/*(* The C spec says that left-hand sides of assignment expressions are unary /*(* The C spec says that left-hand sides of assignment expressions are unary
* expressions. GCC allows cast expressions in there ! *)*/ * expressions. GCC allows cast expressions in there ! *)*/
assignment_expression: /*(* 6.5.16 *)*/ assignment_expression: /*(* 6.5.16 *)*/
| conditional_expression { $1 } | conditional_expression { $1 }
| cast_expression EQ assignment_expression | cast_expression EQ assignment_expression
{ make_expr $sloc (BINARY(ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(ASSIGN, $1, $3)) }
| cast_expression PLUS_EQ assignment_expression | cast_expression PLUS_EQ assignment_expression
{ make_expr $sloc (BINARY(ADD_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(ADD_ASSIGN, $1, $3)) }
| cast_expression MINUS_EQ assignment_expression | cast_expression MINUS_EQ assignment_expression
{ make_expr $sloc (BINARY(SUB_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(SUB_ASSIGN, $1, $3)) }
| cast_expression STAR_EQ assignment_expression | cast_expression STAR_EQ assignment_expression
{ make_expr $sloc (BINARY(MUL_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(MUL_ASSIGN, $1, $3)) }
| cast_expression SLASH_EQ assignment_expression | cast_expression SLASH_EQ assignment_expression
{ make_expr $sloc (BINARY(DIV_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(DIV_ASSIGN, $1, $3)) }
| cast_expression PERCENT_EQ assignment_expression | cast_expression PERCENT_EQ assignment_expression
{ make_expr $sloc (BINARY(MOD_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(MOD_ASSIGN, $1, $3)) }
| cast_expression AND_EQ assignment_expression | cast_expression AND_EQ assignment_expression
{ make_expr $sloc (BINARY(BAND_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(BAND_ASSIGN, $1, $3)) }
| cast_expression PIPE_EQ assignment_expression | cast_expression PIPE_EQ assignment_expression
{ make_expr $sloc (BINARY(BOR_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(BOR_ASSIGN, $1, $3)) }
| cast_expression CIRC_EQ assignment_expression | cast_expression CIRC_EQ assignment_expression
{ make_expr $sloc (BINARY(XOR_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(XOR_ASSIGN, $1, $3)) }
| cast_expression INF_INF_EQ assignment_expression | cast_expression INF_INF_EQ assignment_expression
{ make_expr $sloc (BINARY(SHL_ASSIGN, $1, $3)) } { make_expr $sloc (BINARY(SHL_ASSIGN, $1, $3)) }
| cast_expression SUP_SUP_EQ assignment_expression | cast_expression SUP_SUP_EQ assignment_expression
{ make_expr $sloc (BINARY(SHR_ASSIGN, $1, $3))} { make_expr $sloc (BINARY(SHR_ASSIGN, $1, $3))}
; ;
expression: /*(* 6.5.17 *)*/ /*(* 6.5.17 *)*/
assignment_expression { $1 } expression: assignment_expression { $1 }
;
constant: constant:
CST_INT {CONST_INT (fst $1), snd $1} | CST_INT {CONST_INT (fst $1), snd $1}
| CST_FLOAT {CONST_FLOAT (fst $1), snd $1} | CST_FLOAT {CONST_FLOAT (fst $1), snd $1}
| CST_CHAR {CONST_CHAR (fst $1), snd $1} | CST_CHAR {CONST_CHAR (fst $1), snd $1}
| CST_WCHAR {CONST_WCHAR (fst $1), snd $1} | CST_WCHAR {CONST_WCHAR (fst $1), snd $1}
| string_constant {CONST_STRING (fst $1), snd $1} | string_constant {CONST_STRING (fst $1), snd $1}
| wstring_list {CONST_WSTRING (List.concat (fst $1)), snd $1} | wstring_list {CONST_WSTRING (List.concat (fst $1)), snd $1}
; ;
string_constant: string_constant:
/* Now that we know this constant isn't part of a wstring, convert it /* Now that we know this constant isn't part of a wstring, convert it
back to a string for easy viewing. */ back to a string for easy viewing. */
string_list { | string_list {
let loc = Cil_datatype.Location.of_lexing_loc $loc in let loc = Cil_datatype.Location.of_lexing_loc $loc in
intlist_to_string ~loc (fst $1), snd $1 } intlist_to_string ~loc (fst $1), snd $1
}
; ;
string_list: string_list:
one_string { [fst $1], snd $1 } | one_string { [fst $1], snd $1 }
| one_string string_list { merge_string $1 $2 } | one_string string_list { merge_string $1 $2 }
; ;
wstring_list: wstring_list:
CST_WSTRING { [fst $1], snd $1 } | CST_WSTRING { [fst $1], snd $1 }
| one_string wstring_list { merge_string $1 $2 } | one_string wstring_list { merge_string $1 $2 }
| CST_WSTRING wstring_list { merge_string $1 $2 } | CST_WSTRING wstring_list { merge_string $1 $2 }
| CST_WSTRING string_list { merge_string $1 $2 } | CST_WSTRING string_list { merge_string $1 $2 }
/* If a wstring is present anywhere in the list, the whole is a wstring */ /* If a wstring is present anywhere in the list, the whole is a wstring */
one_string: one_string:
CST_STRING {$1} | CST_STRING {$1}
| FUNCTION__ {(Cabshelper.explodeStringToInts | FUNCTION__ {(Cabshelper.explodeStringToInts !currentFunctionName), $1}
!currentFunctionName), $1} | PRETTY_FUNCTION__ {(Cabshelper.explodeStringToInts !currentFunctionName), $1}
| PRETTY_FUNCTION__ {(Cabshelper.explodeStringToInts
!currentFunctionName), $1}
; ;
init_expression: init_expression:
expression { SINGLE_INIT $1 } | expression { SINGLE_INIT $1 }
| LBRACE initializer_list_opt RBRACE | LBRACE initializer_list_opt RBRACE { COMPOUND_INIT $2}
{ COMPOUND_INIT $2}
initializer_list: /* ISO 6.7.8. Allow a trailing COMMA */ initializer_list: /* ISO 6.7.8. Allow a trailing COMMA */
initializer_single { [$1] } | initializer_single { [$1] }
| initializer_single COMMA initializer_list_opt { $1 :: $3 } | initializer_single COMMA initializer_list_opt { $1 :: $3 }
; ;
initializer_list_opt: initializer_list_opt:
/* empty */ { [] } | /* empty */ { [] }
| initializer_list { $1 } | initializer_list { $1 }
; ;
initializer_single: initializer_single:
init_designators eq_opt init_expression { ($1, $3) } | init_designators eq_opt init_expression { ($1, $3) }
| gcc_init_designators init_expression { ($1, $2) } | gcc_init_designators init_expression { ($1, $2) }
| init_expression { (NEXT_INIT, $1) } | init_expression { (NEXT_INIT, $1) }
; ;
eq_opt: eq_opt:
EQ { () } | EQ { () }
/*(* GCC allows missing = *)*/ /*(* GCC allows missing = *)*/
| /*(* empty *)*/ { () } | /* empty */ { () }
; ;
init_designators: init_designators:
DOT id_or_typename init_designators_opt { INFIELD_INIT($2, $3) } | DOT id_or_typename init_designators_opt { INFIELD_INIT($2, $3) }
| LBRACKET expression RBRACKET init_designators_opt { ATINDEX_INIT($2, $4) } | LBRACKET expression RBRACKET init_designators_opt { ATINDEX_INIT($2, $4) }
| LBRACKET expression ELLIPSIS expression RBRACKET | LBRACKET expression ELLIPSIS expression RBRACKET
{ ATINDEXRANGE_INIT($2, $4) } { ATINDEXRANGE_INIT($2, $4) }
; ;
init_designators_opt: init_designators_opt:
/* empty */ { NEXT_INIT } | /* empty */ { NEXT_INIT }
| init_designators { $1 } | init_designators { $1 }
; ;
gcc_init_designators: /*(* GCC supports these strange things *)*/ gcc_init_designators: /* GCC supports these strange things */
id_or_typename COLON { INFIELD_INIT($1, NEXT_INIT) } | id_or_typename COLON { INFIELD_INIT($1, NEXT_INIT) }
; ;
ghost_arguments_opt: ghost_arguments_opt:
/* empty */ { [] } | /* empty */ { [] }
| ghost_arguments { $1 } | ghost_arguments { $1 }
ghost_arguments: ghost_arguments:
LGHOST LPAREN arguments RPAREN RGHOST { $3 } | LGHOST LPAREN arguments RPAREN RGHOST { $3 }
arguments: arguments:
/* empty */ { [] } | /* empty */ { [] }
| comma_expression { $1 } | comma_expression { $1 }
; ;
opt_expression: opt_expression:
/* empty */ {make_expr $sloc NOTHING} | /* empty */ {make_expr $sloc NOTHING}
| comma_expression {smooth_expression $1 } | comma_expression {smooth_expression $1 }
; ;
comma_expression: comma_expression:
expression { [$1] } | expression { [$1] }
| expression COMMA comma_expression { $1 :: $3 } | expression COMMA comma_expression { $1 :: $3 }
; ;
comma_expression_opt: comma_expression_opt:
/* empty */ { make_expr $sloc NOTHING } | /* empty */ { make_expr $sloc NOTHING }
| comma_expression { smooth_expression $1 } | comma_expression { smooth_expression $1 }
; ;
paren_comma_expression: paren_comma_expression:
LPAREN comma_expression RPAREN { $2 } | LPAREN comma_expression RPAREN { $2 }
; ;
bracket_comma_expression: bracket_comma_expression:
LBRACKET comma_expression RBRACKET { $2 } | LBRACKET comma_expression RBRACKET { $2 }
; ;
/*** statements ***/ /*** statements ***/
generic_block(content): generic_block(content):
block_begin local_labels block_attrs content RBRACE | block_begin local_labels block_attrs content RBRACE
{ { { blabels = $2; battrs = $3; bstmts = $4 }, $1, $5 }
{ blabels = $2;
battrs = $3;
bstmts = $4 },
$1, $5
}
; ;
block: /* ISO 6.8.2 */ block: /* ISO 6.8.2 */
generic_block(block_content) { $1 } | generic_block(block_content) { $1 }
main_block: main_block:
generic_block(main_block_content) { $1 } | generic_block(main_block_content) { $1 }
block_begin: block_begin:
LBRACE { !Lexerhack.push_context (); $1 } | LBRACE { !Lexerhack.push_context (); $1 }
; ;
block_attrs: block_attrs:
/* empty */ { [] } | /* empty */ { [] }
| BLOCKATTRIBUTE paren_attr_list_ne | BLOCKATTRIBUTE paren_attr_list_ne { [("__blockattribute__", $2)] }
{ [("__blockattribute__", $2)] }
; ;
block_content: block_element_list { !Lexerhack.pop_context(); $1 } block_content: block_element_list { !Lexerhack.pop_context(); $1 }
...@@ -910,158 +888,157 @@ main_block_content: block_element_list { ...@@ -910,158 +888,157 @@ main_block_content: block_element_list {
/* statements and declarations in a block, in any order (for C99 support) */ /* statements and declarations in a block, in any order (for C99 support) */
block_element_list: block_element_list:
| annot_list_opt { $1 } | annot_list_opt { $1 }
| annot_list_opt declaration block_element_list | annot_list_opt declaration block_element_list
{ $1 @ no_ghost_stmt (DEFINITION($2)) :: $3 } { $1 @ no_ghost_stmt (DEFINITION($2)) :: $3 }
| annot_list_opt statement block_element_list | annot_list_opt statement block_element_list { $1 @ $2 @ $3 }
{ $1 @ $2 @ $3 } | annot_list_opt pragma block_element_list { $1 @ $3 }
| annot_list_opt pragma block_element_list { $1 @ $3 }
; ;
annot_list_opt: annot_list_opt:
/* empty */ { [] } | /* empty */ { [] }
| annot_list { $1 } | annot_list { $1 }
; ;
annot_list: annot_list:
CODE_ANNOT annot_list_opt { no_ghost [Cabs.CODE_ANNOT $1] @ $2} | CODE_ANNOT annot_list_opt { no_ghost [Cabs.CODE_ANNOT $1] @ $2}
| LGHOST block_element_list RGHOST annot_list_opt | LGHOST block_element_list RGHOST annot_list_opt { (in_ghost $2) @ $4 }
{ (in_ghost $2) @ $4 }
; ;
local_labels: local_labels:
/* empty */ { [] } | /* empty */ { [] }
| LABEL__ local_label_names SEMICOLON local_labels { $2 @ $4 } | LABEL__ local_label_names SEMICOLON local_labels { $2 @ $4 }
; ;
local_label_names: local_label_names:
id_or_typename_as_id { [ $1 ] } | id_or_typename_as_id { [ $1 ] }
| id_or_typename_as_id COMMA local_label_names { $1 :: $3 } | id_or_typename_as_id COMMA local_label_names { $1 :: $3 }
; ;
annotated_statement: annotated_statement:
| statement { $1 } | statement { $1 }
| annot_list statement { $1 @ $2 } | annot_list statement { $1 @ $2 }
; ;
else_part: else_part:
/* empty */ { | /* empty */ {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost_stmt (NOP loc) no_ghost_stmt (NOP loc)
} }
%prec if_no_else /* To attach the next else to the current if */ %prec if_no_else /* To attach the next else to the current if */
| ELSE annotated_statement | ELSE annotated_statement { in_block $loc($2) $2 }
{ in_block $loc($2) $2 } | LGHOST_ELSE annotated_statement RGHOST
| LGHOST_ELSE annotated_statement RGHOST
{ in_ghost_block ~battrs:[ (Cil.frama_c_ghost_else , []) ] $2 } { in_ghost_block ~battrs:[ (Cil.frama_c_ghost_else , []) ] $2 }
%prec ghost_else_no_else /* To force the non ghost else to be attached to the current if */ %prec ghost_else_no_else /* To force the non ghost else to be attached to the current if */
| LGHOST_ELSE annotated_statement RGHOST ELSE annotated_statement | LGHOST_ELSE annotated_statement RGHOST ELSE annotated_statement {
{ let loc = Cil_datatype.Location.of_lexing_loc $sloc in
let loc = Cil_datatype.Location.of_lexing_loc $sloc in Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use ~source:(fst loc)
Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use ~source:(fst loc) "Invalid ghost else ignored" ;
"Invalid ghost else ignored" ; in_block $loc($5) $5
in_block $loc($5) $5 }
}
statement: statement:
SEMICOLON { no_ghost [NOP $1] } | SEMICOLON { no_ghost [NOP $1] }
| SPEC annotated_statement | SPEC annotated_statement {
{ let bs = $2 in
let bs = $2 in match Logic_lexer.spec $1 with
match Logic_lexer.spec $1 with | Some (loc',spec) ->
| Some (loc',spec) -> let spec = no_ghost [Cabs.CODE_SPEC (spec, (fst $1, loc'))] in
let spec = no_ghost [Cabs.CODE_SPEC (spec, (fst $1, loc'))] in spec @ $2
spec @ $2 | None -> bs
| None -> bs }
} | comma_expression SEMICOLON {
| comma_expression SEMICOLON let loc = Cil_datatype.Location.of_lexing_loc $sloc in
{ let loc = Cil_datatype.Location.of_lexing_loc $sloc in no_ghost [COMPUTATION (smooth_expression $1,loc)]
no_ghost [COMPUTATION (smooth_expression $1,loc)]} }
| block { let (x,y,z) = $1 in no_ghost [BLOCK (x, y, z)]} | block { let (x,y,z) = $1 in no_ghost [BLOCK (x, y, z)] }
| IF paren_comma_expression annotated_statement else_part | IF paren_comma_expression annotated_statement else_part {
{ let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [IF (smooth_expression $2, no_ghost [IF (smooth_expression $2, in_block $loc($3) $3, $4, loc)]
in_block $loc($3) $3, $4, loc)]} }
| SWITCH paren_comma_expression annotated_statement | SWITCH paren_comma_expression annotated_statement {
{ let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [SWITCH (smooth_expression $2, in_block $loc($3) $3, loc)]} no_ghost [SWITCH (smooth_expression $2, in_block $loc($3) $3, loc)]
| opt_loop_annotations }
WHILE paren_comma_expression annotated_statement | opt_loop_annotations WHILE paren_comma_expression annotated_statement {
{ let first = Cil_datatype.Position.of_lexing_pos $startpos($2) in let first = Cil_datatype.Position.of_lexing_pos $startpos($2) in
let last = Cil_datatype.Position.of_lexing_pos $endpos in let last = Cil_datatype.Position.of_lexing_pos $endpos in
no_ghost [WHILE ($1, smooth_expression $3, in_block $loc($4) $4, (first,last))] } no_ghost [WHILE ($1, smooth_expression $3, in_block $loc($4) $4, (first,last))]
| opt_loop_annotations }
DO annotated_statement WHILE paren_comma_expression SEMICOLON | opt_loop_annotations DO annotated_statement WHILE paren_comma_expression SEMICOLON {
{ let first = Cil_datatype.Position.of_lexing_pos $startpos($2) in let first = Cil_datatype.Position.of_lexing_pos $startpos($2) in
let last = Cil_datatype.Position.of_lexing_pos $endpos in let last = Cil_datatype.Position.of_lexing_pos $endpos in
no_ghost [DOWHILE ($1, smooth_expression $5, in_block $loc($3) $3, (first,last))]} no_ghost [DOWHILE ($1, smooth_expression $5, in_block $loc($3) $3, (first,last))]
| opt_loop_annotations }
FOR LPAREN for_clause opt_expression | opt_loop_annotations FOR LPAREN for_clause opt_expression SEMICOLON
SEMICOLON opt_expression RPAREN annotated_statement opt_expression RPAREN annotated_statement {
{ let first = Cil_datatype.Position.of_lexing_pos $startpos($2) in let first = Cil_datatype.Position.of_lexing_pos $startpos($2) in
let last = Cil_datatype.Position.of_lexing_pos $endpos in let last = Cil_datatype.Position.of_lexing_pos $endpos in
no_ghost [FOR ($1, $4, $5, $7, in_block $loc($9) $9, (first,last))]} no_ghost [FOR ($1, $4, $5, $7, in_block $loc($9) $9, (first,last))]
| id_or_typename_as_id COLON attribute_nocv_list annotated_statement }
{(* The only attribute that should appear here | id_or_typename_as_id COLON attribute_nocv_list annotated_statement {
is "unused". For now, we drop this on the (* The only attribute that should appear here is "unused". For now, we drop
floor, since unused labels are usually this on the floor, since unused labels are usually removed anyways by
removed anyways by Rmtmps. *) Rmtmps.
let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in *)
match $4 with let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
| [] -> (* should not happen if grammar is written correctly *) match $4 with
Errorloc.parse_error ~loc "empty statement after label" | [] -> (* should not happen if grammar is written correctly *)
| s :: others -> no_ghost [LABEL($1,s,loc)] @ others } Errorloc.parse_error ~loc "empty statement after label"
| s :: others -> no_ghost [LABEL($1,s,loc)] @ others
| CASE expression COLON annotated_statement }
{ let loc = Cil_datatype.Location.of_lexing_loc $sloc in | CASE expression COLON annotated_statement {
no_ghost [CASE ($2, in_block $loc($4) $4, loc)]} let loc = Cil_datatype.Location.of_lexing_loc $sloc in
| CASE expression ELLIPSIS expression COLON annotated_statement no_ghost [CASE ($2, in_block $loc($4) $4, loc)]
{ let loc = Cil_datatype.Location.of_lexing_loc $sloc in }
no_ghost [CASERANGE ($2, $4, in_block $loc($6) $6, loc)]} | CASE expression ELLIPSIS expression COLON annotated_statement {
| DEFAULT COLON annotated_statement let loc = Cil_datatype.Location.of_lexing_loc $sloc in
{ let loc = Cil_datatype.Location.of_lexing_loc $sloc in no_ghost [CASERANGE ($2, $4, in_block $loc($6) $6, loc)]
no_ghost [DEFAULT (in_block $loc($3) $3, loc)]} }
| RETURN SEMICOLON { | DEFAULT COLON annotated_statement {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [RETURN ({ expr_loc = loc; expr_node = NOTHING}, loc)] no_ghost [DEFAULT (in_block $loc($3) $3, loc)]
} }
| RETURN comma_expression SEMICOLON { | RETURN SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [RETURN (smooth_expression $2, loc)] no_ghost [RETURN ({ expr_loc = loc; expr_node = NOTHING}, loc)]
} }
| BREAK SEMICOLON { | RETURN comma_expression SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [BREAK loc] no_ghost [RETURN (smooth_expression $2, loc)]
} }
| CONTINUE SEMICOLON { | BREAK SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [CONTINUE loc] no_ghost [BREAK loc]
} }
| GOTO id_or_typename_as_id SEMICOLON { | CONTINUE SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [GOTO ($2, loc)] no_ghost [CONTINUE loc]
} }
| GOTO STAR comma_expression SEMICOLON { | GOTO id_or_typename_as_id SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [COMPGOTO (smooth_expression $3, loc) ] no_ghost [GOTO ($2, loc)]
} }
| ASM GOTO asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON { | GOTO STAR comma_expression SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $loc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [ASM ($3, mk_asm_templates $5, $6, loc)] no_ghost [COMPGOTO (smooth_expression $3, loc) ]
} }
| ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON { | ASM GOTO asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $loc in
no_ghost [ASM ($2, mk_asm_templates $4, $5, loc)] no_ghost [ASM ($3, mk_asm_templates $5, $6, loc)]
} }
| ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in
no_ghost [ASM ($2, mk_asm_templates $4, $5, loc)]
}
; ;
opt_loop_annotations: opt_loop_annotations:
/* epsilon */ { [] } | /* empty */ { [] }
| loop_annotations { $1 } | loop_annotations { $1 }
; ;
loop_annotations: loop_annotations: loop_annotation { $1 }
loop_annotation { $1 }
/* Not in ACSL Grammar /* Not in ACSL Grammar
| loop_annotation loop_annotations | loop_annotation loop_annotations
{ { Cil_types.invariant = $1.Cil_types.invariant @ $2.Cil_types.invariant; { { Cil_types.invariant = $1.Cil_types.invariant @ $2.Cil_types.invariant;
...@@ -1073,26 +1050,26 @@ loop_annotations: ...@@ -1073,26 +1050,26 @@ loop_annotations:
; ;
loop_annotation: loop_annotation:
LOOP_ANNOT { fst $1 } | LOOP_ANNOT { fst $1 }
; ;
for_clause: for_clause:
opt_expression SEMICOLON { FC_EXP $1 } | opt_expression SEMICOLON { FC_EXP $1 }
| declaration { FC_DECL $1 } | declaration { FC_DECL $1 }
; ;
ghost_parameter_opt: ghost_parameter_opt:
/* empty */ {[]} | /* empty */ {[]}
| ghost_parameter {$1} | ghost_parameter {$1}
; ;
ghost_parameter: ghost_parameter:
LGHOST parameter_list_startscope rest_par_list RPAREN RGHOST { let (l, _) = $3 in l } | LGHOST parameter_list_startscope rest_par_list RPAREN RGHOST
{ let (l, _) = $3 in l }
; ;
declaration: /* ISO 6.7.*/ declaration: /* ISO 6.7.*/
spec=ioption(SPEC) specif=decl_spec_list decls=init_declarator_list? SEMICOLON | spec=ioption(SPEC) specif=decl_spec_list decls=init_declarator_list? SEMICOLON {
{
let loc = Cil_datatype.Location.of_lexing_loc ($symbolstartpos,$endpos) in let loc = Cil_datatype.Location.of_lexing_loc ($symbolstartpos,$endpos) in
let decls = Option.value ~default:[] decls in let decls = Option.value ~default:[] decls in
if !Lexerhack.is_typedef () && decls = [] then begin if !Lexerhack.is_typedef () && decls = [] then begin
...@@ -1103,103 +1080,84 @@ declaration: /* ISO 6.7.*/ ...@@ -1103,103 +1080,84 @@ declaration: /* ISO 6.7.*/
!Lexerhack.reset_typedef(); !Lexerhack.reset_typedef();
doDeclaration spec loc (fst specif) decls doDeclaration spec loc (fst specif) decls
} }
| static_assert_declaration SEMICOLON | static_assert_declaration SEMICOLON
{ let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) } { let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) }
; ;
static_assert_declaration: static_assert_declaration:
| STATIC_ASSERT LPAREN expression RPAREN { ($3, "", $1) }
| STATIC_ASSERT LPAREN expression RPAREN | STATIC_ASSERT LPAREN expression COMMA string_constant RPAREN { ($3, fst $5, $1) }
{
($3, "", $1)
}
| STATIC_ASSERT LPAREN expression COMMA string_constant RPAREN
{
($3, fst $5, $1)
}
; ;
generic_selection: /* ISO C11 6.5.1.1 */ generic_selection: /* ISO C11 6.5.1.1 */
| GENERIC LPAREN assignment_expression COMMA generic_association_list RPAREN | GENERIC LPAREN assignment_expression COMMA generic_association_list RPAREN
{ { ($3, $5) }
($3, $5) | GENERIC LPAREN assignment_expression RPAREN {
} let loc = Cil_datatype.Location.of_lexing_loc $loc in
| GENERIC LPAREN assignment_expression RPAREN Errorloc.parse_error ~loc
{ "_Generic requires at least one generic association";
let loc = Cil_datatype.Location.of_lexing_loc $loc in }
Errorloc.parse_error ~loc
"_Generic requires at least one generic association";
}
generic_association_list: generic_association_list:
| generic_association { [ $1 ] } | generic_association { [ $1 ] }
| generic_association COMMA generic_association_list { $1 :: $3 } | generic_association COMMA generic_association_list { $1 :: $3 }
generic_association: generic_association:
| type_name COLON assignment_expression | type_name COLON assignment_expression { let s, d = $1 in (Some (s, d), $3) }
{ | DEFAULT COLON assignment_expression { (None, $3) }
let s, d = $1 in
(Some (s, d), $3)
}
| DEFAULT COLON assignment_expression
{
(None, $3)
}
; ;
init_declarator_list: init_declarator_list:
decl_and_init_decl_attr_list { register_symbol_class $1; $1 } | decl_and_init_decl_attr_list { register_symbol_class $1; $1 }
; ;
decl_and_init_decl_attr_list: decl_and_init_decl_attr_list:
init_declarator { [$1] } | init_declarator { [$1] }
| init_declarator COMMA init_declarator_attr_list { $1 :: $3 } | init_declarator COMMA init_declarator_attr_list { $1 :: $3 }
; ;
init_declarator_attr_list: init_declarator_attr_list:
init_declarator_attr { [ $1 ] } | init_declarator_attr { [ $1 ] }
| init_declarator_attr COMMA init_declarator_attr_list { $1 :: $3 } | init_declarator_attr COMMA init_declarator_attr_list { $1 :: $3 }
; ;
init_declarator_attr: init_declarator_attr:
attribute_nocv_list init_declarator { | attribute_nocv_list init_declarator {
let ((name, decl, attrs, loc), init) = $2 in let ((name, decl, attrs, loc), init) = $2 in
((name, PARENTYPE ($1,decl,[]), attrs, loc), init) ((name, PARENTYPE ($1,decl,[]), attrs, loc), init)
} }
; ;
init_declarator: /* ISO 6.7 */ init_declarator: /* ISO 6.7 */
declarator { ($1, NO_INIT) } | declarator { ($1, NO_INIT) }
| declarator EQ init_expression | declarator EQ init_expression { ($1, $3) }
{ ($1, $3) }
; ;
// C standard specifiers without type specifiers // C standard specifiers without type specifiers
decl_spec_wo_type_nor_attr: /* ISO 6.7 */ decl_spec_wo_type_nor_attr: /* ISO 6.7 */
/* ISO 6.7.1 */ // ISO 6.7.1
| TYPEDEF { !Lexerhack.set_typedef(); SpecTypedef, $1 } | TYPEDEF { !Lexerhack.set_typedef(); SpecTypedef, $1 }
| EXTERN { SpecStorage EXTERN, $1 } | EXTERN { SpecStorage EXTERN, $1 }
| STATIC { SpecStorage STATIC, $1 } | STATIC { SpecStorage STATIC, $1 }
| AUTO { SpecStorage AUTO, $1 } | AUTO { SpecStorage AUTO, $1 }
| REGISTER { SpecStorage REGISTER, $1} | REGISTER { SpecStorage REGISTER, $1}
/* ISO 6.7.4 */ // ISO 6.7.4
| INLINE { SpecInline, $1 } | INLINE { SpecInline, $1 }
| NORETURN { SpecAttr (("noreturn",[])), $1 } | NORETURN { SpecAttr (("noreturn",[])), $1 }
| cvspec { $1 } // ISO 6.7.3
| cvspec { $1 }
; ;
// GCC allows attributes in decl specifiers // GCC allows attributes in decl specifiers
decl_spec_attribute: decl_spec_attribute:
| attribute_nocv { SpecAttr (fst $1), snd $1 } | attribute_nocv { SpecAttr (fst $1), snd $1 }
; ;
// All possible decl specifiers // All possible decl specifiers
any_decl_spec: any_decl_spec:
| decl_spec_wo_type_nor_attr { fst $1 } | decl_spec_wo_type_nor_attr { fst $1 }
| decl_spec_attribute { fst $1 } | decl_spec_attribute { fst $1 }
| type_spec { SpecType(fst $1) } | type_spec { SpecType(fst $1) }
/* The specifier list of decls cannot contain only GCC attribute specifiers. It /* The specifier list of decls cannot contain only GCC attribute specifiers. It
must contain at least one type specifier or any other C standard specifier. must contain at least one type specifier or any other C standard specifier.
...@@ -1207,9 +1165,8 @@ any_decl_spec: ...@@ -1207,9 +1165,8 @@ any_decl_spec:
and allow any specifier or empty. */ and allow any specifier or empty. */
decl_spec_list: decl_spec_list:
| decl_spec_wo_type_nor_attr decl_spec_list_opt { fst $1 :: $2, snd $1 } | decl_spec_wo_type_nor_attr decl_spec_list_opt { fst $1 :: $2, snd $1 }
| decl_spec_attribute decl_spec_list { fst $1 :: fst $2, snd $1 } | decl_spec_attribute decl_spec_list { fst $1 :: fst $2, snd $1 }
| type_spec pragma* (* pragma accepted by GCC *) decl_spec_list_opt_no_named | type_spec pragma* (* pragma accepted by GCC *) decl_spec_list_opt_no_named {
{
let pragmas = $2 in let pragmas = $2 in
if pragmas != [] then begin if pragmas != [] then begin
let loc = Cabshelper.get_definitionloc (List.hd pragmas) in let loc = Cabshelper.get_definitionloc (List.hd pragmas) in
...@@ -1224,9 +1181,8 @@ decl_spec_list: ...@@ -1224,9 +1181,8 @@ decl_spec_list:
C standard specifier. */ C standard specifier. */
decl_spec_list_no_restriction: decl_spec_list_no_restriction:
| decl_spec_wo_type_nor_attr decl_spec_list_opt { fst $1 :: $2, snd $1 } | decl_spec_wo_type_nor_attr decl_spec_list_opt { fst $1 :: $2, snd $1 }
| decl_spec_attribute decl_spec_list_opt { fst $1 :: $2, snd $1 } | decl_spec_attribute decl_spec_list_opt { fst $1 :: $2, snd $1 }
| type_spec pragma* (* pragma accepted by GCC *) decl_spec_list_opt_no_named | type_spec pragma* (* pragma accepted by GCC *) decl_spec_list_opt_no_named {
{
let pragmas = $2 in let pragmas = $2 in
if pragmas != [] then begin if pragmas != [] then begin
let loc = Cabshelper.get_definitionloc (List.hd pragmas) in let loc = Cabshelper.get_definitionloc (List.hd pragmas) in
...@@ -1238,222 +1194,225 @@ decl_spec_list_no_restriction: ...@@ -1238,222 +1194,225 @@ decl_spec_list_no_restriction:
} }
/* (* In most cases if we see a NAMED_TYPE we must shift it. Thus we declare /* (* In most cases if we see a NAMED_TYPE we must shift it. Thus we declare
* NAMED_TYPE to have right associativity *) */ * NAMED_TYPE to have right associativity *) */
decl_spec_list_opt: decl_spec_list_opt:
/* empty */ { [] } %prec NAMED_TYPE | /* empty */ { [] } %prec NAMED_TYPE
| decl_spec_list_no_restriction { fst $1 } | decl_spec_list_no_restriction { fst $1 }
; ;
/* (* We add this separate rule to handle the special case when an appearance /* (* We add this separate rule to handle the special case when an appearance
* of NAMED_TYPE should not be considered as part of the specifiers but as * of NAMED_TYPE should not be considered as part of the specifiers but as
* part of the declarator. IDENT has higher precedence than NAMED_TYPE *) * part of the declarator. IDENT has higher precedence than NAMED_TYPE *)
*/ */
decl_spec_list_opt_no_named: decl_spec_list_opt_no_named:
/* empty */ { [] } %prec IDENT | /* empty */ { [] } %prec IDENT
| any_decl_spec decl_spec_list_opt_no_named { $1 :: $2 } | any_decl_spec decl_spec_list_opt_no_named { $1 :: $2 }
; ;
type_spec: /* ISO 6.7.2 */ type_spec: /* ISO 6.7.2 */
VOID { Tvoid, $1} | VOID { Tvoid, $1}
| CHAR { Tchar, $1 } | CHAR { Tchar, $1 }
| BOOL { Tbool, $1 } | BOOL { Tbool, $1 }
| SHORT { Tshort, $1 } | SHORT { Tshort, $1 }
| INT { Tint, $1 } | INT { Tint, $1 }
| LONG { Tlong, $1 } | LONG { Tlong, $1 }
| INT64 { Tint64, $1 } | INT64 { Tint64, $1 }
| FLOAT { Tfloat, $1 } | FLOAT { Tfloat, $1 }
| DOUBLE { Tdouble, $1 } | DOUBLE { Tdouble, $1 }
| SIGNED { Tsigned, $1 } | SIGNED { Tsigned, $1 }
| UNSIGNED { Tunsigned, $1 } | UNSIGNED { Tunsigned, $1 }
| STRUCT id_or_typename | STRUCT id_or_typename
{ Tstruct ($2, None, []), $1 } { Tstruct ($2, None, []), $1 }
| STRUCT just_attributes id_or_typename | STRUCT just_attributes id_or_typename
{ Tstruct ($3, None, $2), $1 } { Tstruct ($3, None, $2), $1 }
| STRUCT id_or_typename LBRACE struct_decl_list RBRACE | STRUCT id_or_typename LBRACE struct_decl_list RBRACE
{ Tstruct ($2, Some $4, []), $1 } { Tstruct ($2, Some $4, []), $1 }
| STRUCT LBRACE struct_decl_list RBRACE | STRUCT LBRACE struct_decl_list RBRACE
{ Tstruct ("", Some $3, []), $1 } { Tstruct ("", Some $3, []), $1 }
| STRUCT just_attributes id_or_typename LBRACE struct_decl_list RBRACE | STRUCT just_attributes id_or_typename LBRACE struct_decl_list RBRACE
{ Tstruct ($3, Some $5, $2), $1 } { Tstruct ($3, Some $5, $2), $1 }
| STRUCT just_attributes LBRACE struct_decl_list RBRACE | STRUCT just_attributes LBRACE struct_decl_list RBRACE
{ Tstruct ("", Some $4, $2), $1 } { Tstruct ("", Some $4, $2), $1 }
| UNION id_or_typename | UNION id_or_typename
{ Tunion ($2, None, []), $1 } { Tunion ($2, None, []), $1 }
| UNION id_or_typename LBRACE struct_decl_list RBRACE | UNION id_or_typename LBRACE struct_decl_list RBRACE
{ Tunion ($2, Some $4, []), $1 } { Tunion ($2, Some $4, []), $1 }
| UNION LBRACE struct_decl_list RBRACE | UNION LBRACE struct_decl_list RBRACE
{ Tunion ("", Some $3, []), $1 } { Tunion ("", Some $3, []), $1 }
| UNION just_attributes id_or_typename LBRACE struct_decl_list RBRACE | UNION just_attributes id_or_typename LBRACE struct_decl_list RBRACE
{ Tunion ($3, Some $5, $2), $1 } { Tunion ($3, Some $5, $2), $1 }
| UNION just_attributes LBRACE struct_decl_list RBRACE | UNION just_attributes LBRACE struct_decl_list RBRACE
{ Tunion ("", Some $4, $2), $1 } { Tunion ("", Some $4, $2), $1 }
| ENUM id_or_typename | ENUM id_or_typename
{ Tenum ($2, None, []), $1 } { Tenum ($2, None, []), $1 }
| ENUM id_or_typename LBRACE enum_list maybecomma RBRACE | ENUM id_or_typename LBRACE enum_list maybecomma RBRACE
{ Tenum ($2, Some $4, []), $1 } { Tenum ($2, Some $4, []), $1 }
| ENUM LBRACE enum_list maybecomma RBRACE | ENUM LBRACE enum_list maybecomma RBRACE
{ Tenum ("", Some $3, []), $1 } { Tenum ("", Some $3, []), $1 }
| ENUM just_attributes id_or_typename LBRACE enum_list maybecomma RBRACE | ENUM just_attributes id_or_typename LBRACE enum_list maybecomma RBRACE
{ Tenum ($3, Some $5, $2), $1 } { Tenum ($3, Some $5, $2), $1 }
| ENUM just_attributes LBRACE enum_list maybecomma RBRACE | ENUM just_attributes LBRACE enum_list maybecomma RBRACE
{ Tenum ("", Some $4, $2), $1 } { Tenum ("", Some $4, $2), $1 }
| NAMED_TYPE { | NAMED_TYPE {
(Tnamed $1, Cil_datatype.Location.of_lexing_loc $sloc) (Tnamed $1, Cil_datatype.Location.of_lexing_loc $sloc)
} }
| TYPEOF LPAREN expression RPAREN { TtypeofE $3, $1 } | TYPEOF LPAREN expression RPAREN { TtypeofE $3, $1 }
| TYPEOF LPAREN type_name RPAREN { let s, d = $3 in | TYPEOF LPAREN type_name RPAREN { let s, d = $3 in
TtypeofT (s, d), $1 } TtypeofT (s, d), $1 }
; ;
struct_decl_list: /* (* ISO 6.7.2. Except that we allow empty structs. We
* also allow missing field names. *) /* (* ISO 6.7.2. Except that we allow empty structs. We
*/ * also allow missing field names. *) */
/* empty */ { [] } struct_decl_list:
| decl_spec_list SEMICOLON struct_decl_list | /* empty */ { [] }
{ FIELD (fst $1, | decl_spec_list SEMICOLON struct_decl_list
[(missingFieldDecl, None)]) :: $3 } { FIELD (fst $1, [(missingFieldDecl, None)]) :: $3 }
/*(* GCC allows extra semicolons *)*/ /*(* GCC allows extra semicolons *)*/
| SEMICOLON struct_decl_list | SEMICOLON struct_decl_list { $2 }
{ $2 } | decl_spec_list field_decl_list SEMICOLON struct_decl_list
| decl_spec_list field_decl_list SEMICOLON struct_decl_list { FIELD (fst $1, $2) :: $4 }
{ FIELD (fst $1, $2)
:: $4 }
/*(* MSVC allows pragmas in strange places *)*/ /*(* MSVC allows pragmas in strange places *)*/
| pragma struct_decl_list { $2 } | pragma struct_decl_list { $2 }
/*(* C11 allows static_assert-declaration *)*/ /*(* C11 allows static_assert-declaration *)*/
| static_assert_declaration { | static_assert_declaration {
let (e, m, loc) = $1 in let (e, m, loc) = $1 in
[ STATIC_ASSERT_FG (e, m, loc) ] [ STATIC_ASSERT_FG (e, m, loc) ]
} }
| static_assert_declaration SEMICOLON struct_decl_list {
| static_assert_declaration SEMICOLON struct_decl_list { let (e, m, loc) = $1 in
let (e, m, loc) = $1 in STATIC_ASSERT_FG (e, m, loc) :: $3
STATIC_ASSERT_FG (e, m, loc) :: $3 }
}
; ;
field_decl_list: /* (* ISO 6.7.2 *) */ field_decl_list: /* (* ISO 6.7.2 *) */
field_decl { [$1] } | field_decl { [$1] }
| field_decl COMMA field_decl_list { $1 :: $3 } | field_decl COMMA field_decl_list { $1 :: $3 }
; ;
field_decl: /* (* ISO 6.7.2. Except that we allow unnamed fields. *) */ field_decl: /* (* ISO 6.7.2. Except that we allow unnamed fields. *) */
| declarator { ($1, None) } | declarator { ($1, None) }
| declarator COLON expression attributes | declarator COLON expression attributes {
{ let (n,decl,al,loc) = $1 in let (n,decl,al,loc) = $1 in
let al' = al @ $4 in let al' = al @ $4 in
((n,decl,al',loc), Some $3) } ((n,decl,al',loc), Some $3)
| COLON expression { (missingFieldDecl, Some $2) } }
| COLON expression { (missingFieldDecl, Some $2) }
; ;
enum_list: /* (* ISO 6.7.2.2 *) */ enum_list: /* (* ISO 6.7.2.2 *) */
enumerator {[$1]} | enumerator {[$1]}
| enum_list COMMA enumerator {$1 @ [$3]} | enum_list COMMA enumerator {$1 @ [$3]}
; ;
enumerator: enumerator:
IDENT { | IDENT {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
($1, { expr_node = NOTHING; expr_loc = loc }, loc) ($1, { expr_node = NOTHING; expr_loc = loc }, loc)
} }
| IDENT just_attributes { | IDENT just_attributes {
let attrs = $2 in let attrs = $2 in
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let loc = Cil_datatype.Location.of_lexing_loc $sloc in
Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes
~source:(fst loc) ~source:(fst loc)
"Discarding attributes in enumerator (unsupported feature): %a" "Discarding attributes in enumerator (unsupported feature): %a"
Cprint.print_attributes attrs; Cprint.print_attributes attrs;
($1, { expr_node = NOTHING; expr_loc = loc }, loc) ($1, { expr_node = NOTHING; expr_loc = loc }, loc)
} }
| IDENT EQ expression { | IDENT EQ expression { ($1, $3, Cil_datatype.Location.of_lexing_loc $sloc) }
($1, $3, Cil_datatype.Location.of_lexing_loc $sloc) | IDENT just_attributes EQ expression {
} let attrs = $2 in
| IDENT just_attributes EQ expression { let loc = Cil_datatype.Location.of_lexing_loc $sloc in
let attrs = $2 in Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes
let loc = Cil_datatype.Location.of_lexing_loc $sloc in ~source:(fst loc)
Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes "Discarding attributes in enumerator (unsupported feature): %a"
~source:(fst loc) Cprint.print_attributes attrs;
"Discarding attributes in enumerator (unsupported feature): %a" ($1, $4, loc)
Cprint.print_attributes attrs; }
($1, $4, loc)
}
; ;
declarator: /* (* ISO 6.7.5. Plus Microsoft declarators.*) */ declarator: /* (* ISO 6.7.5. Plus Microsoft declarators.*) */
pointer_opt direct_decl attributes_with_asm { | pointer_opt direct_decl attributes_with_asm {
let (n, decl, loc) = $2 in let (n, decl, loc) = $2 in
(n, applyPointer $1 decl, $3, loc) (n, applyPointer $1 decl, $3, loc)
} }
; ;
attributes_or_static: /* 6.7.5.2/3 */ attributes_or_static: /* 6.7.5.2/3 */
| attributes comma_expression_opt { $1,$2 } | attributes comma_expression_opt { $1,$2 }
| attribute attributes STATIC comma_expression { | attribute attributes STATIC comma_expression
fst $1::$2 @ ["static",[]], smooth_expression $4 { fst $1::$2 @ ["static",[]], smooth_expression $4 }
} | STATIC attributes comma_expression
| STATIC attributes comma_expression { { ("static",[]) :: $2, smooth_expression $3 }
("static",[]) :: $2, smooth_expression $3
}
; ;
direct_decl: /* (* ISO 6.7.5 *) */ direct_decl: /* (* ISO 6.7.5 *) */
/* (* We want to be able to redefine named /* (* We want to be able to redefine named types as variable names *) */
* types as variable names *) */ | id_or_typename { ($1, JUSTBASE, Cil_datatype.Location.of_lexing_loc $sloc) }
| id_or_typename { ($1, JUSTBASE, Cil_datatype.Location.of_lexing_loc $sloc) }
| LPAREN attributes declarator RPAREN {
| LPAREN attributes declarator RPAREN let (n,decl,al,loc) = $3 in
{ let (n,decl,al,loc) = $3 in (n, PARENTYPE($2,decl,al), loc)
(n, PARENTYPE($2,decl,al), loc) } }
| direct_decl LBRACKET attributes_or_static RBRACKET {
| direct_decl LBRACKET attributes_or_static RBRACKET let (n, decl, loc) = $1 in
{ let (n, decl, loc) = $1 in let (attrs, size) = $3 in
let (attrs, size) = $3 in (n, ARRAY(decl, attrs, size), loc)
(n, ARRAY(decl, attrs, size), loc) } }
| direct_decl LPAREN RPAREN ghost_parameter_opt { | direct_decl LPAREN RPAREN ghost_parameter_opt {
let (n,decl,loc) = $1 in (n, PROTO(decl,[],$4,false), loc) let (n,decl,loc) = $1 in (n, PROTO(decl,[],$4,false), loc)
} }
| direct_decl parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt | direct_decl parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt {
{ let (n, decl, loc) = $1 in let (n, decl, loc) = $1 in
let (params, isva) = $3 in let (params, isva) = $3 in
let ghost = $5 in let ghost = $5 in
!Lexerhack.pop_context (); !Lexerhack.pop_context ();
(n, PROTO(decl, params, ghost, isva), loc) (n, PROTO(decl, params, ghost, isva), loc)
} }
; ;
parameter_list_startscope: parameter_list_startscope:
LPAREN { !Lexerhack.push_context () } | LPAREN { !Lexerhack.push_context () }
; ;
rest_par_list: rest_par_list:
| parameter_decl rest_par_list1 { let (params, isva) = $2 in | parameter_decl rest_par_list1 {
($1 :: params, isva) let (params, isva) = $2 in
} ($1 :: params, isva)
}
; ;
rest_par_list1: rest_par_list1:
/* empty */ { ([], false) } | /* empty */ { ([], false) }
| COMMA ELLIPSIS { ([], true) } | COMMA ELLIPSIS { ([], true) }
| COMMA parameter_decl rest_par_list1 { let (params, isva) = $3 in | COMMA parameter_decl rest_par_list1 {
($2 :: params, isva) let (params, isva) = $3 in
} ($2 :: params, isva)
}
; ;
parameter_decl: /* (* ISO 6.7.5 *) */ parameter_decl: /* (* ISO 6.7.5 *) */
decl_spec_list declarator { (fst $1, $2) } | decl_spec_list declarator { (fst $1, $2) }
| decl_spec_list abstract_decl { let d, a = $2 in | decl_spec_list abstract_decl {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in let d, a = $2 in
(fst $1, ("", d, a, loc)) } let loc = Cil_datatype.Location.of_lexing_loc $sloc in
| decl_spec_list { let loc = Cil_datatype.Location.of_lexing_loc $sloc in (fst $1, ("", d, a, loc))
(fst $1, ("", JUSTBASE, [], loc)) } }
| LPAREN parameter_decl RPAREN { $2 } | decl_spec_list {
let loc = Cil_datatype.Location.of_lexing_loc $sloc in
(fst $1, ("", JUSTBASE, [], loc))
}
| LPAREN parameter_decl RPAREN { $2 }
; ;
/* (* Old style prototypes. Like a declarator *) */ /* (* Old style prototypes. Like a declarator *) */
old_proto_decl: old_proto_decl:
pointer_opt direct_old_proto_decl { | pointer_opt direct_old_proto_decl {
let (n, decl, a, loc) = $2 in let (n, decl, a, loc) = $2 in
(n, applyPointer $1 decl, a, loc) (n, applyPointer $1 decl, a, loc)
} }
; ;
direct_old_proto_decl: direct_old_proto_decl:
...@@ -1462,7 +1421,6 @@ direct_old_proto_decl: ...@@ -1462,7 +1421,6 @@ direct_old_proto_decl:
let par_decl, isva = doOldParDecl floc $3 $5 in let par_decl, isva = doOldParDecl floc $3 $5 in
(n, PROTO(decl, par_decl, [],isva), ["FC_OLDSTYLEPROTO",[]], floc) (n, PROTO(decl, par_decl, [],isva), ["FC_OLDSTYLEPROTO",[]], floc)
} }
/* (* appears sometimesm but generates a shift-reduce conflict. *) /* (* appears sometimesm but generates a shift-reduce conflict. *)
| LPAREN STAR direct_decl LPAREN old_parameter_list_ne RPAREN RPAREN | LPAREN STAR direct_decl LPAREN old_parameter_list_ne RPAREN RPAREN
LPAREN RPAREN old_pardef_list { LPAREN RPAREN old_pardef_list {
...@@ -1473,36 +1431,35 @@ direct_old_proto_decl: ...@@ -1473,36 +1431,35 @@ direct_old_proto_decl:
; ;
old_parameter_list_ne: old_parameter_list_ne:
| IDENT { [$1] } | IDENT { [$1] }
| IDENT COMMA old_parameter_list_ne { $1::$3 } | IDENT COMMA old_parameter_list_ne { $1::$3 }
; ;
old_pardef_list: old_pardef_list:
/* empty */ { ([], false) } | /* empty */ { ([], false) }
| decl_spec_list old_pardef SEMICOLON ELLIPSIS | decl_spec_list old_pardef SEMICOLON ELLIPSIS { ([(fst $1, $2)], true) }
{ ([(fst $1, $2)], true) } | decl_spec_list old_pardef SEMICOLON old_pardef_list {
| decl_spec_list old_pardef SEMICOLON old_pardef_list let rest, isva = $4 in
{ let rest, isva = $4 in ((fst $1, $2) :: rest, isva)
((fst $1, $2) :: rest, isva) }
}
; ;
old_pardef: old_pardef:
declarator { [$1] } | declarator { [$1] }
| declarator COMMA old_pardef { $1 :: $3 } | declarator COMMA old_pardef { $1 :: $3 }
; ;
pointer: /* (* ISO 6.7.5 *) */ pointer: /* (* ISO 6.7.5 *) */
STAR attributes pointer_opt { $2 :: $3 } | STAR attributes pointer_opt { $2 :: $3 }
; ;
pointer_opt: pointer_opt:
/**/ { [] } | /* empty */ { [] }
| pointer { $1 } | pointer { $1 }
; ;
type_name: /* (* ISO 6.7.6 *) */ type_name: /* (* ISO 6.7.6 *) */
specif=decl_spec_list name=abstract_decl { | specif=decl_spec_list name=abstract_decl {
let d, a = name in let d, a = name in
if a <> [] then begin if a <> [] then begin
let loc = Cil_datatype.Location.of_lexing_loc ($loc(name)) in let loc = Cil_datatype.Location.of_lexing_loc ($loc(name)) in
...@@ -1510,88 +1467,86 @@ type_name: /* (* ISO 6.7.6 *) */ ...@@ -1510,88 +1467,86 @@ type_name: /* (* ISO 6.7.6 *) */
end; end;
(fst specif, d) (fst specif, d)
} }
| decl_spec_list { (fst $1, JUSTBASE) } | decl_spec_list { (fst $1, JUSTBASE) }
; ;
abstract_decl: /* (* ISO 6.7.6. *) */ abstract_decl: /* (* ISO 6.7.6. *) */
pointer_opt abs_direct_decl attributes { applyPointer $1 $2, $3 } | pointer_opt abs_direct_decl attributes { applyPointer $1 $2, $3 }
| pointer { applyPointer $1 JUSTBASE, [] } | pointer { applyPointer $1 JUSTBASE, [] }
; ;
abs_direct_decl: /* (* ISO 6.7.6. We do not support optional declarator for abs_direct_decl: /* (* ISO 6.7.6. We do not support optional declarator for
* functions. Plus Microsoft attributes. See the * functions. Plus Microsoft attributes. See the
* discussion for declarator. *) */ * discussion for declarator. *) */
| LPAREN attributes abstract_decl RPAREN | LPAREN attributes abstract_decl RPAREN {
{ let d, a = $3 in let d, a = $3 in
PARENTYPE ($2, d, a) PARENTYPE ($2, d, a)
} }
| abs_direct_decl_opt LBRACKET comma_expression_opt RBRACKET
| abs_direct_decl_opt LBRACKET comma_expression_opt RBRACKET { ARRAY($1, [], $3) }
{ ARRAY($1, [], $3) }
/*(* The next should be abs_direct_decl_opt but we get conflicts *)*/ /*(* The next should be abs_direct_decl_opt but we get conflicts *)*/
| abs_direct_decl parameter_list_startscope rest_par_list RPAREN | abs_direct_decl parameter_list_startscope rest_par_list RPAREN {
{ let (params, isva) = $3 in let (params, isva) = $3 in
!Lexerhack.pop_context (); !Lexerhack.pop_context ();
PROTO ($1, params,[], isva) PROTO ($1, params,[], isva)
} }
| abs_direct_decl LPAREN RPAREN { PROTO ($1, [],[], false) } | abs_direct_decl LPAREN RPAREN { PROTO ($1, [],[], false) }
; ;
abs_direct_decl_opt: abs_direct_decl_opt:
abs_direct_decl { $1 } | abs_direct_decl { $1 }
| /* empty */ { JUSTBASE } | /* empty */ { JUSTBASE }
;
function_def: /* (* ISO 6.9.1 *) */
s=ioption(SPEC) fn=function_def_start b=main_block
{
let (loc, specs, decl) = fn in
let spec_loc =
Option.bind s
(fun s ->
let loc = fst s in
Option.map
(fun (loc', spec) -> spec, (loc, loc'))
(Logic_lexer.spec s))
in
currentFunctionName := "<__FUNCTION__ used outside any functions>";
doFunctionDef spec_loc loc (trd3 b) specs decl (fst3 b)
}
; ;
function_def_start: /* (* ISO 6.9.1 *) */ function_def: /* (* ISO 6.9.1 *) */
decl_spec_list declarator | s=ioption(SPEC) fn=function_def_start b=main_block {
{ announceFunctionName $2; let (loc, specs, decl) = fn in
(fourth4 $2, fst $1, $2) let spec_loc =
} Option.bind s
(fun s ->
let loc = fst s in
Option.map
(fun (loc', spec) -> spec, (loc, loc'))
(Logic_lexer.spec s))
in
currentFunctionName := "<__FUNCTION__ used outside any functions>";
doFunctionDef spec_loc loc (trd3 b) specs decl (fst3 b)
}
;
function_def_start: /* (* ISO 6.9.1 *) */
| decl_spec_list declarator {
announceFunctionName $2;
(fourth4 $2, fst $1, $2)
}
/* (* Old-style function prototype *) */ /* (* Old-style function prototype *) */
| decl_spec_list old_proto_decl | decl_spec_list old_proto_decl {
{ announceFunctionName $2; announceFunctionName $2;
(snd $1, fst $1, $2) (snd $1, fst $1, $2)
} }
/* (* New-style function that does not have a return type *) */ /* (* New-style function that does not have a return type *) */
| IDENT parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt | IDENT parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt{
{ let (params, isva) = $3 in let (params, isva) = $3 in
let ghost = $5 in let ghost = $5 in
let floc = Cil_datatype.Location.of_lexing_loc $loc($1) in let floc = Cil_datatype.Location.of_lexing_loc $loc($1) in
let fdec = ($1, PROTO(JUSTBASE, params, ghost, isva), [], floc) in let fdec = ($1, PROTO(JUSTBASE, params, ghost, isva), [], floc) in
announceFunctionName fdec; announceFunctionName fdec;
(* Default is int type *) (* Default is int type *)
let defSpec = [SpecType Tint] in (floc, defSpec, fdec) let defSpec = [SpecType Tint] in (floc, defSpec, fdec)
} }
/* (* No return type and old-style parameter list *) */ /* (* No return type and old-style parameter list *) */
| IDENT LPAREN old_parameter_list_ne RPAREN old_pardef_list | IDENT LPAREN old_parameter_list_ne RPAREN old_pardef_list {
{ (* Convert pardecl to new style *) (* Convert pardecl to new style *)
let floc = Cil_datatype.Location.of_lexing_loc $loc($1) in let floc = Cil_datatype.Location.of_lexing_loc $loc($1) in
let pardecl, isva = doOldParDecl floc $3 $5 in let pardecl, isva = doOldParDecl floc $3 $5 in
(* Make the function declarator *) (* Make the function declarator *)
let fdec = ($1, PROTO(JUSTBASE, pardecl,[],isva), [], floc) in let fdec = ($1, PROTO(JUSTBASE, pardecl,[],isva), [], floc) in
announceFunctionName fdec; announceFunctionName fdec;
(* Default is int type *) (* Default is int type *)
(floc, [SpecType Tint], fdec) (floc, [SpecType Tint], fdec)
} }
| IDENT LPAREN RPAREN ghost_parameter_opt | IDENT LPAREN RPAREN ghost_parameter_opt {
{
let floc = Cil_datatype.Location.of_lexing_loc $loc($1) in let floc = Cil_datatype.Location.of_lexing_loc $loc($1) in
let fdec = ($1, PROTO(JUSTBASE,[],$4,false),[],floc) in let fdec = ($1, PROTO(JUSTBASE,[],$4,false),[],floc) in
announceFunctionName fdec; announceFunctionName fdec;
...@@ -1601,337 +1556,338 @@ function_def_start: /* (* ISO 6.9.1 *) */ ...@@ -1601,337 +1556,338 @@ function_def_start: /* (* ISO 6.9.1 *) */
/* const/volatile as type specifier elements */ /* const/volatile as type specifier elements */
cvspec: cvspec:
| CONST { SpecCV(CV_CONST), $1 } | CONST { SpecCV(CV_CONST), $1 }
| VOLATILE { SpecCV(CV_VOLATILE), $1 } | VOLATILE { SpecCV(CV_VOLATILE), $1 }
| RESTRICT { SpecCV(CV_RESTRICT), $1 } | RESTRICT { SpecCV(CV_RESTRICT), $1 }
| GHOST { SpecCV(CV_GHOST), $1 } | GHOST { SpecCV(CV_GHOST), $1 }
| ATTRIBUTE_ANNOT | ATTRIBUTE_ANNOT {
{ let annot, loc = $1 in
let annot, loc = $1 in if String.compare annot "\\ghost" = 0 then begin
if String.compare annot "\\ghost" = 0 then begin Errorloc.parse_error ~loc "Use of \\ghost out of ghost code"
Errorloc.parse_error ~loc "Use of \\ghost out of ghost code" end else
end else SpecCV(CV_ATTRIBUTE_ANNOT annot), loc
SpecCV(CV_ATTRIBUTE_ANNOT annot), loc }
}
; ;
/*** GCC attributes ***/ /*** GCC attributes ***/
attributes: attributes:
/* empty */ { []} | /* empty */ { [] }
| attribute attributes { fst $1 :: $2 } | attribute attributes { fst $1 :: $2 }
; ;
/* (* In some contexts we can have an inline assembly to specify the name to /* (* In some contexts we can have an inline assembly to specify the name to
* be used for a global. We treat this as a name attribute *) */ * be used for a global. We treat this as a name attribute *) */
attributes_with_asm: attributes_with_asm:
/* empty */ { [] } | /* empty */ { [] }
| attribute attributes_with_asm { fst $1 :: $2 } | attribute attributes_with_asm { fst $1 :: $2 }
| ASM LPAREN string_constant RPAREN attributes { | ASM LPAREN string_constant RPAREN attributes {
let loc = Cil_datatype.Location.of_lexing_loc $loc($3) in let loc = Cil_datatype.Location.of_lexing_loc $loc($3) in
("__asm__", ("__asm__",
[{ expr_node = CONSTANT(CONST_STRING (fst $3)); expr_loc = loc}]) [{ expr_node = CONSTANT(CONST_STRING (fst $3)); expr_loc = loc}])
:: $5 :: $5
} }
; ;
/* things like __attribute__, but no const/volatile */ /* things like __attribute__, but no const/volatile */
attribute_nocv: attribute_nocv:
ATTRIBUTE LPAREN paren_attr_list RPAREN | ATTRIBUTE LPAREN paren_attr_list RPAREN { ("__attribute__", $3), $1 }
{ ("__attribute__", $3), $1 } | NOP_ATTRIBUTE { ("__attribute__", []), $1 }
| NOP_ATTRIBUTE { ("__attribute__", []), $1 } | DECLSPEC paren_attr_list_ne { ("__declspec", $2), $1 }
| DECLSPEC paren_attr_list_ne { ("__declspec", $2), $1 } | MSATTR { (fst $1, []), snd $1 }
| MSATTR { (fst $1, []), snd $1 } // ISO 6.7.3
/* ISO 6.7.3 */ | THREAD { ("__thread", []), $1 }
| THREAD { ("__thread", []), $1 } | THREAD_LOCAL { ("__thread", [make_expr $sloc (VARIABLE "c11")]), $1 }
| THREAD_LOCAL { ("__thread",
[make_expr $sloc (VARIABLE "c11")]),
$1 }
; ;
attribute_nocv_list: attribute_nocv_list:
/* empty */ { []} | /* empty */ { [] }
| attribute_nocv attribute_nocv_list { fst $1 :: $2 } | attribute_nocv attribute_nocv_list { fst $1 :: $2 }
; ;
/* __attribute__ plus const/volatile */ /* __attribute__ plus const/volatile */
attribute: attribute:
attribute_nocv { $1 } | attribute_nocv { $1 }
| CONST { ("const", []), $1 } | CONST { ("const", []), $1 }
| RESTRICT { ("restrict",[]), $1 } | RESTRICT { ("restrict",[]), $1 }
| VOLATILE { ("volatile",[]), $1 } | VOLATILE { ("volatile",[]), $1 }
| GHOST { ("ghost",[]), $1 } | GHOST { ("ghost",[]), $1 }
| ATTRIBUTE_ANNOT { let annot, loc = $1 in (mk_attr_annot annot), loc } | ATTRIBUTE_ANNOT { let annot, loc = $1 in (mk_attr_annot annot), loc }
; ;
/* (* sm: I need something that just includes __attribute__ and nothing more, /* (* sm: I need something that just includes __attribute__ and nothing more,
* to support them appearing between the 'struct' keyword and the type name. * to support them appearing between the 'struct' keyword and the type name.
* Actually, a declspec can appear there as well (on MSVC) *) */ * Actually, a declspec can appear there as well (on MSVC) *) */
just_attribute: just_attribute:
ATTRIBUTE LPAREN paren_attr_list RPAREN | ATTRIBUTE LPAREN paren_attr_list RPAREN { ("__attribute__", $3) }
{ ("__attribute__", $3) } | DECLSPEC paren_attr_list_ne { ("__declspec", $2) }
| DECLSPEC paren_attr_list_ne { ("__declspec", $2) }
; ;
/* this can't be empty, b/c I folded that possibility into the calling /* this can't be empty, b/c I folded that possibility into the calling
* productions to avoid some S/R conflicts */ * productions to avoid some S/R conflicts */
just_attributes: just_attributes:
just_attribute { [$1] } | just_attribute { [$1] }
| just_attribute just_attributes { $1 :: $2 } | just_attribute just_attributes { $1 :: $2 }
; ;
/** (* PRAGMAS and ATTRIBUTES *) ***/ /** (* PRAGMAS and ATTRIBUTES *) ***/
pragma: pragma:
| PRAGMA PRAGMA_EOL { | PRAGMA PRAGMA_EOL { PRAGMA (make_expr $sloc (VARIABLE ("")), $1) }
PRAGMA (make_expr $sloc (VARIABLE ("")), $1) | PRAGMA attr PRAGMA_EOL { PRAGMA ($2, $1) }
} | PRAGMA attr SEMICOLON PRAGMA_EOL { PRAGMA ($2, $1) }
| PRAGMA attr PRAGMA_EOL { PRAGMA ($2, $1) } | PRAGMA_LINE { PRAGMA (make_expr $sloc (VARIABLE (fst $1)), snd $1) }
| PRAGMA attr SEMICOLON PRAGMA_EOL { PRAGMA ($2, $1) }
| PRAGMA_LINE {
PRAGMA (make_expr $sloc (VARIABLE (fst $1)), snd $1)
}
; ;
/* (* We want to allow certain strange things that occur in pragmas, so we /* (* We want to allow certain strange things that occur in pragmas, so we
* cannot use directly the language of expressions *) */ * cannot use directly the language of expressions *) */
var_attr: var_attr:
| IDENT { make_expr $sloc (VARIABLE $1) } | IDENT { make_expr $sloc (VARIABLE $1) }
| NAMED_TYPE { make_expr $sloc (VARIABLE $1) } | NAMED_TYPE { make_expr $sloc (VARIABLE $1) }
| DEFAULT COLON CST_INT { make_expr $sloc (VARIABLE ("default:" ^ fst $3)) } | DEFAULT COLON CST_INT { make_expr $sloc (VARIABLE ("default:" ^ fst $3)) }
/* Const when it appears in attribute lists, is translated to aconst */ /* Const when it appears in attribute lists, is translated to aconst */
| CONST { make_expr $sloc (VARIABLE "aconst") } | CONST { make_expr $sloc (VARIABLE "aconst") }
/*(** GCC allows this as an attribute for functions, synonym for noreturn **)*/ /*(** GCC allows this as an attribute for functions, synonym for noreturn **)*/
| VOLATILE { make_expr $sloc (VARIABLE ("__noreturn__")) } | VOLATILE { make_expr $sloc (VARIABLE ("__noreturn__")) }
| CST_INT COLON CST_INT { make_expr $sloc (VARIABLE (fst $1 ^ ":" ^ fst $3)) } | CST_INT COLON CST_INT { make_expr $sloc (VARIABLE (fst $1 ^ ":" ^ fst $3)) }
; ;
basic_attr: basic_attr:
| CST_INT { make_expr $sloc (CONSTANT(CONST_INT (fst $1))) } | CST_INT { make_expr $sloc (CONSTANT(CONST_INT (fst $1))) }
| CST_FLOAT { make_expr $sloc (CONSTANT(CONST_FLOAT(fst $1))) } | CST_FLOAT { make_expr $sloc (CONSTANT(CONST_FLOAT(fst $1))) }
| var_attr { $1 } | var_attr { $1 }
; ;
basic_attr_list_ne: basic_attr_list_ne:
basic_attr { [$1] } | basic_attr { [$1] }
| basic_attr basic_attr_list_ne { $1::$2 } | basic_attr basic_attr_list_ne { $1::$2 }
; ;
parameter_attr_list_ne: parameter_attr_list_ne:
basic_attr_list_ne { $1 } | basic_attr_list_ne { $1 }
| basic_attr_list_ne string_constant { | basic_attr_list_ne string_constant {
$1 @ [make_expr $sloc (CONSTANT(CONST_STRING (fst $2)))] $1 @ [make_expr $sloc (CONSTANT(CONST_STRING (fst $2)))]
} }
| basic_attr_list_ne string_constant parameter_attr_list_ne { | basic_attr_list_ne string_constant parameter_attr_list_ne {
$1 @ ([make_expr $sloc (CONSTANT(CONST_STRING (fst $2)))] @ $3) $1 @ ([make_expr $sloc (CONSTANT(CONST_STRING (fst $2)))] @ $3)
} }
; ;
param_attr_list_ne: param_attr_list_ne:
parameter_attr_list_ne { $1 } | parameter_attr_list_ne { $1 }
| string_constant { [make_expr $sloc (CONSTANT(CONST_STRING (fst $1)))] } | string_constant { [make_expr $sloc (CONSTANT(CONST_STRING (fst $1)))] }
; ;
primary_attr: primary_attr:
basic_attr { $1 } | basic_attr { $1 }
| LPAREN attr RPAREN { $2 } | LPAREN attr RPAREN { $2 }
| string_constant { make_expr $sloc (CONSTANT(CONST_STRING (fst $1))) } | string_constant { make_expr $sloc (CONSTANT(CONST_STRING (fst $1))) }
; ;
postfix_attr:
primary_attr { $1 }
| id_or_typename_as_id paren_attr_list_ne {
let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
make_expr $sloc (CALL({ expr_loc = loc; expr_node = VARIABLE $1}, $2,[])) }
/* (* use a VARIABLE "" so that the parentheses are printed *) */
| id_or_typename_as_id LPAREN RPAREN {
let loc1 = Cil_datatype.Location.of_lexing_loc $loc($1) in
let loc2 =
Cil_datatype.Position.of_lexing_pos $startpos($2),
Cil_datatype.Position.of_lexing_pos $endpos($3)
in
let f = { expr_node = VARIABLE $1; expr_loc = loc1 } in
let arg = { expr_node = VARIABLE ""; expr_loc = loc2 } in
make_expr $sloc (CALL(f, [arg],[]))
}
/* (* use a VARIABLE "" so that the parameters are printed without
* parentheses nor comma *) */
| basic_attr param_attr_list_ne {
let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
make_expr $sloc (CALL({ expr_node = VARIABLE ""; expr_loc = loc}, $1::$2,[])) }
| postfix_attr ARROW id_or_typename { make_expr $sloc (MEMBEROFPTR ($1, $3))} postfix_attr:
| postfix_attr DOT id_or_typename { make_expr $sloc (MEMBEROF ($1, $3)) } | primary_attr { $1 }
| postfix_attr LBRACKET attr RBRACKET { make_expr $sloc (INDEX ($1, $3)) } | id_or_typename_as_id paren_attr_list_ne {
let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
make_expr $sloc (CALL({ expr_loc = loc; expr_node = VARIABLE $1}, $2,[]))
}
/* (* use a VARIABLE "" so that the parentheses are printed *) */
| id_or_typename_as_id LPAREN RPAREN {
let loc1 = Cil_datatype.Location.of_lexing_loc $loc($1) in
let loc2 =
Cil_datatype.Position.of_lexing_pos $startpos($2),
Cil_datatype.Position.of_lexing_pos $endpos($3)
in
let f = { expr_node = VARIABLE $1; expr_loc = loc1 } in
let arg = { expr_node = VARIABLE ""; expr_loc = loc2 } in
make_expr $sloc (CALL(f, [arg],[]))
}
/* (* use a VARIABLE "" so that the parameters are printed without
* parentheses nor comma *) */
| basic_attr param_attr_list_ne {
let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
make_expr $sloc (CALL({ expr_node = VARIABLE ""; expr_loc = loc}, $1::$2,[]))
}
| postfix_attr ARROW id_or_typename { make_expr $sloc (MEMBEROFPTR ($1, $3))}
| postfix_attr DOT id_or_typename { make_expr $sloc (MEMBEROF ($1, $3)) }
| postfix_attr LBRACKET attr RBRACKET { make_expr $sloc (INDEX ($1, $3)) }
; ;
/*(* Since in attributes we use both IDENT and NAMED_TYPE as indentifiers, /*(* Since in attributes we use both IDENT and NAMED_TYPE as indentifiers,
* that leads to conflicts for SIZEOF and ALIGNOF. In those cases we require * that leads to conflicts for SIZEOF and ALIGNOF. In those cases we require
* that their arguments be expressions, not attributes *)*/ * that their arguments be expressions, not attributes *)*/
unary_attr: unary_attr:
postfix_attr { $1 } | postfix_attr { $1 }
| SIZEOF unary_expression { make_expr $sloc (EXPR_SIZEOF $2) } | SIZEOF unary_expression { make_expr $sloc (EXPR_SIZEOF $2) }
| SIZEOF LPAREN type_name RPAREN | SIZEOF LPAREN type_name RPAREN {
{let b, d = $3 in let b, d = $3 in
make_expr $sloc (TYPE_SIZEOF (b, d)) } make_expr $sloc (TYPE_SIZEOF (b, d))
}
| ALIGNOF unary_expression {make_expr $sloc (EXPR_ALIGNOF $2) } | ALIGNOF unary_expression {make_expr $sloc (EXPR_ALIGNOF $2) }
| ALIGNOF LPAREN type_name RPAREN {let b, d = $3 in | ALIGNOF LPAREN type_name RPAREN {
make_expr $sloc (TYPE_ALIGNOF (b, d)) } let b, d = $3 in
| PLUS cast_attr {make_expr $sloc (UNARY (PLUS, $2))} make_expr $sloc (TYPE_ALIGNOF (b, d))
| MINUS cast_attr {make_expr $sloc (UNARY (MINUS, $2)) } }
| STAR cast_attr {make_expr $sloc (UNARY (MEMOF, $2)) } | PLUS cast_attr { make_expr $sloc (UNARY (PLUS, $2)) }
| AND cast_attr | MINUS cast_attr { make_expr $sloc (UNARY (MINUS, $2)) }
{ make_expr $sloc (UNARY (ADDROF, $2)) } | STAR cast_attr { make_expr $sloc (UNARY (MEMOF, $2)) }
| EXCLAM cast_attr { make_expr $sloc (UNARY (NOT, $2)) } | AND cast_attr { make_expr $sloc (UNARY (ADDROF, $2)) }
| TILDE cast_attr { make_expr $sloc (UNARY (BNOT, $2)) } | EXCLAM cast_attr { make_expr $sloc (UNARY (NOT, $2)) }
| TILDE cast_attr { make_expr $sloc (UNARY (BNOT, $2)) }
; ;
cast_attr: cast_attr: unary_attr { $1 }
unary_attr { $1 }
;
multiplicative_attr: multiplicative_attr:
cast_attr { $1 } | cast_attr { $1 }
| multiplicative_attr STAR cast_attr {make_expr $sloc (BINARY(MUL ,$1 , $3))} | multiplicative_attr STAR cast_attr {make_expr $sloc (BINARY(MUL ,$1 , $3))}
| multiplicative_attr SLASH cast_attr {make_expr $sloc (BINARY(DIV ,$1 , $3))} | multiplicative_attr SLASH cast_attr {make_expr $sloc (BINARY(DIV ,$1 , $3))}
| multiplicative_attr PERCENT cast_attr {make_expr $sloc (BINARY(MOD ,$1 , $3))} | multiplicative_attr PERCENT cast_attr {make_expr $sloc (BINARY(MOD ,$1 , $3))}
; ;
additive_attr: additive_attr:
multiplicative_attr { $1 } | multiplicative_attr { $1 }
| additive_attr PLUS multiplicative_attr {make_expr $sloc (BINARY(ADD ,$1 , $3))} | additive_attr PLUS multiplicative_attr {make_expr $sloc (BINARY(ADD ,$1 , $3))}
| additive_attr MINUS multiplicative_attr {make_expr $sloc (BINARY(SUB ,$1 , $3))} | additive_attr MINUS multiplicative_attr {make_expr $sloc (BINARY(SUB ,$1 , $3))}
; ;
shift_attr: shift_attr:
additive_attr { $1 } | additive_attr { $1 }
| shift_attr INF_INF additive_attr {make_expr $sloc (BINARY(SHL ,$1 , $3))} | shift_attr INF_INF additive_attr {make_expr $sloc (BINARY(SHL ,$1 , $3))}
| shift_attr SUP_SUP additive_attr {make_expr $sloc (BINARY(SHR ,$1 , $3))} | shift_attr SUP_SUP additive_attr {make_expr $sloc (BINARY(SHR ,$1 , $3))}
; ;
relational_attr: relational_attr:
shift_attr { $1 } | shift_attr { $1 }
| relational_attr INF shift_attr {make_expr $sloc (BINARY(LT ,$1 , $3))} | relational_attr INF shift_attr {make_expr $sloc (BINARY(LT ,$1 , $3))}
| relational_attr SUP shift_attr {make_expr $sloc (BINARY(GT ,$1 , $3))} | relational_attr SUP shift_attr {make_expr $sloc (BINARY(GT ,$1 , $3))}
| relational_attr INF_EQ shift_attr {make_expr $sloc (BINARY(LE ,$1 , $3))} | relational_attr INF_EQ shift_attr {make_expr $sloc (BINARY(LE ,$1 , $3))}
| relational_attr SUP_EQ shift_attr {make_expr $sloc (BINARY(GE ,$1 , $3))} | relational_attr SUP_EQ shift_attr {make_expr $sloc (BINARY(GE ,$1 , $3))}
; ;
equality_attr: equality_attr:
relational_attr { $1 } | relational_attr { $1 }
| equality_attr EQ_EQ relational_attr {make_expr $sloc (BINARY(EQ ,$1 , $3))} | equality_attr EQ_EQ relational_attr {make_expr $sloc (BINARY(EQ ,$1 , $3))}
| equality_attr EXCLAM_EQ relational_attr {make_expr $sloc (BINARY(NE ,$1 , $3))} | equality_attr EXCLAM_EQ relational_attr {make_expr $sloc (BINARY(NE ,$1 , $3))}
; ;
bitwise_and_attr: bitwise_and_attr:
equality_attr { $1 } | equality_attr { $1 }
| bitwise_and_attr AND equality_attr {make_expr $sloc (BINARY(BAND ,$1 , $3))} | bitwise_and_attr AND equality_attr {make_expr $sloc (BINARY(BAND ,$1 , $3))}
; ;
bitwise_xor_attr: bitwise_xor_attr:
bitwise_and_attr { $1 } | bitwise_and_attr { $1 }
| bitwise_xor_attr CIRC bitwise_and_attr {make_expr $sloc (BINARY(XOR ,$1 , $3))} | bitwise_xor_attr CIRC bitwise_and_attr {make_expr $sloc (BINARY(XOR ,$1 , $3))}
; ;
bitwise_or_attr: bitwise_or_attr:
bitwise_xor_attr { $1 } | bitwise_xor_attr { $1 }
| bitwise_or_attr PIPE bitwise_xor_attr {make_expr $sloc (BINARY(BOR ,$1 , $3))} | bitwise_or_attr PIPE bitwise_xor_attr {make_expr $sloc (BINARY(BOR ,$1 , $3))}
; ;
logical_and_attr: logical_and_attr:
bitwise_or_attr { $1 } | bitwise_or_attr { $1 }
| logical_and_attr AND_AND bitwise_or_attr | logical_and_attr AND_AND bitwise_or_attr {make_expr $sloc (BINARY(AND ,$1 , $3))}
{make_expr $sloc (BINARY(AND ,$1 , $3))}
; ;
logical_or_attr: logical_or_attr:
logical_and_attr { $1 } | logical_and_attr { $1 }
| logical_or_attr PIPE_PIPE logical_and_attr | logical_or_attr PIPE_PIPE logical_and_attr {make_expr $sloc (BINARY(OR ,$1 , $3))}
{make_expr $sloc (BINARY(OR ,$1 , $3))}
; ;
conditional_attr: conditional_attr:
logical_or_attr { $1 } | logical_or_attr { $1 }
| logical_or_attr QUEST attr_test conditional_attr COLON2 conditional_attr | logical_or_attr QUEST attr_test conditional_attr COLON2 conditional_attr
{ make_expr $sloc (QUESTION($1, $4, $6)) } { make_expr $sloc (QUESTION($1, $4, $6)) }
assign_attr: assign_attr:
conditional_attr { $1 } | conditional_attr { $1 }
| conditional_attr EQ conditional_attr { make_expr $sloc (BINARY(ASSIGN,$1,$3)) } | conditional_attr EQ conditional_attr { make_expr $sloc (BINARY(ASSIGN,$1,$3)) }
/* hack to avoid shift reduce conflict in attribute parsing. */ /* hack to avoid shift reduce conflict in attribute parsing. */
attr_test: attr_test:
| /* empty */ { Cabshelper.push_attr_test () } | /* empty */ { Cabshelper.push_attr_test () }
attr: assign_attr { $1 } attr: assign_attr { $1 }
;
attr_list_ne: attr_list_ne:
| attr { [$1] } | attr { [$1] }
| attr COMMA attr_list_ne { $1 :: $3 } | attr COMMA attr_list_ne { $1 :: $3 }
; ;
attr_list: attr_list:
/* empty */ { [] } | /* empty */ { [] }
| attr_list_ne { $1 } | attr_list_ne { $1 }
; ;
paren_attr_list_ne: paren_attr_list_ne:
LPAREN attr_list_ne RPAREN { $2 } | LPAREN attr_list_ne RPAREN { $2 }
; ;
paren_attr_list: paren_attr_list:
LPAREN attr_list RPAREN { $2 } | LPAREN attr_list RPAREN { $2 }
; ;
/*** GCC ASM instructions ***/ /*** GCC ASM instructions ***/
asmattr: asmattr:
/* empty */ { [] } | /* empty */ { [] }
| VOLATILE asmattr { ("volatile", []) :: $2 } | VOLATILE asmattr { ("volatile", []) :: $2 }
| CONST asmattr { ("const", []) :: $2 } | CONST asmattr { ("const", []) :: $2 }
; ;
asmtemplate: asmtemplate:
line=one_string { | line=one_string {
let loc = Cil_datatype.Location.of_lexing_loc $loc in let loc = Cil_datatype.Location.of_lexing_loc $loc in
[intlist_to_string ~loc [fst line]] [intlist_to_string ~loc [fst line]]
} }
| line=one_string rest=asmtemplate { | line=one_string rest=asmtemplate {
let loc = Cil_datatype.Location.of_lexing_loc $loc(line) in let loc = Cil_datatype.Location.of_lexing_loc $loc(line) in
intlist_to_string ~loc [fst line] :: rest intlist_to_string ~loc [fst line] :: rest
} }
; ;
asmoutputs: asmoutputs:
/* empty */ { None } | /* empty */ { None }
| COLON asmoperands asminputs | COLON asmoperands asminputs {
{ let (ins, (clobs,labels)) = $3 in let (ins, (clobs,labels)) = $3 in
Some {aoutputs = $2; ainputs = ins; aclobbers = clobs; Some {aoutputs = $2; ainputs = ins; aclobbers = clobs; alabels = labels }
alabels = labels } } }
; ;
asmoperands: asmoperands:
/* empty */ { [] } | /* empty */ { [] }
| asmoperandsne { List.rev $1 } | asmoperandsne { List.rev $1 }
; ;
asmoperandsne: asmoperandsne:
asmoperand { [$1] } | asmoperand { [$1] }
| asmoperandsne COMMA asmoperand { $3 :: $1 } | asmoperandsne COMMA asmoperand { $3 :: $1 }
; ;
asmoperand: asmoperand:
asmopname string_constant LPAREN expression RPAREN { ($1, fst $2, $4) } | asmopname string_constant LPAREN expression RPAREN { ($1, fst $2, $4) }
; ;
asminputs: asminputs:
/* empty */ { ([], ([],[])) } | /* empty */ { ([], ([],[])) }
| COLON asmoperands asmclobber | COLON asmoperands asmclobber { ($2, $3) }
{ ($2, $3) }
; ;
asmopname: asmopname:
/* empty */ { None } | /* empty */ { None }
| LBRACKET IDENT RBRACKET { Some $2 } | LBRACKET IDENT RBRACKET { Some $2 }
; ;
asmclobber: asmclobber:
/* empty */ { [],[] } | /* empty */ { [],[] }
| COLON asmlabels { [],$2 } | COLON asmlabels { [],$2 }
| COLON asmcloberlst_ne asmlabels { $2,$3 } | COLON asmcloberlst_ne asmlabels { $2,$3 }
; ;
asmcloberlst_ne: asmcloberlst_ne:
string_constant { [fst $1] } | string_constant { [fst $1] }
| string_constant COMMA asmcloberlst_ne { fst $1 :: $3 } | string_constant COMMA asmcloberlst_ne { fst $1 :: $3 }
; ;
asmlabels: asmlabels:
| /* empty */ { [] } | /* empty */ { [] }
| COLON local_label_names { $2 } | COLON local_label_names { $2 }
%% %%
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