Appendix F - Grammar

F1. Introduction

Here is a grammar of the C language as subsetted and extended by eCv. It is based on the grammar in the ISO C90 standard, with the following changes:

The dangling-else ambiguity has been resolved
The grammar for switch statements has been rewritten to limit switch statements to the form supported by eCv
Grammatical constructs not supported by eCv have been removed (e.g. K&R-style function parameter declarations)
Some C99 consructs have been included
The C++ cast operators (other than dynamic_cast) have been included
Additional eCv specification constructs and eCv expression types have been added

In the following grammar, keywords are displayed in bold. Other terminal symbols have UPPERCASE names and the following meanings:

ASSOP	One of += -= *= /= %= <<= >>= &= \|= ^=
BOOLLITERAL	false or true
CASTOPERATOR	One of const_cast reinterpret_cast static_cast
CHARLITERAL	A character literal token
EMPTYSTRINGLITERAL	The empty string literal, i.e. ""
IDENTIFIER	An identifier
INTEGERLITERAL	An integer literal token
NONEMPTYSTRINGLITERAL	Any string literal except the empty string literal
REALLITERAL	A float or double literal token
OP4	+ or -
OP5	% or /
OPINCDEC	++ or --
OPLEGE	>= or <=
OPSHIFT	>> or <<
PREDEFTYPE	One of bool float void
SIGNMODIFIER	signed or unsigned
SIZEOF	sizeof or min_sizeof
STORAGECLASS	One of auto extern register static
STRUCTORUNION	struct or union
THATorANY	that or any
TYPEDEF_NAME	An IDENTIFIER that has previously been used to name a type in a typedef declaration
TYPEOP	minof or maxof

The symbol 'Empty' means the empty string. The goal symbol is translation_unit. Comments are italicised.

F2. Grammar

primary_expression:
    IDENTIFIER;
    c_stringLiteral;
    INTEGERLITERAL;
    REALLITERAL;
    CHARLITERAL;
    BOOLLITERAL;
    '(' CExpression ')';
    '(' let_decl_list CExpression ')';
    result.

let_decl_list:
let_declaration;
let_decl_list let_declaration.

let_declaration:
let IDENTIFIER '=' CExpression ';'.

postfix_expression:
    primary_expression;
    BoundOperatorExpr] postfix_expression c_index;
    postfix_expression '(' ')';
    postfix_expression '(' argument_expression_list ')';
    postfix_expression '.' IDENTIFIER;
    postfix_expression '->' IDENTIFIER;
    postfix_expression OPINCDEC;
    '(' type_name ')' '{' initializer_list '}';
    '(' type_name ')' '{' initializer_list ',' '}';
    CASTOPERATOR '<' type_name '>' '(' CExpression ')';
    not_null '(' assignment_expression ')';
    disjoint '(' argument_expression_list ')'.

c_index:
'[' CExpression ']'.

argument_expression_list:
assignment_expression;
argument_expression_list ',' assignment_expression.

unary_expression:
    postfix_expression;
    old postfix_expression;
    OPINCDEC unary_expression;
    unary_operator cast_expression;
    '&' cast_expression;
    '!' cast_expression;
    SIZEOF unary_expression;
    SIZEOF '(' type_name ')';
    TYPEOP '(' type_name ')';
    default '(' type_name ')';
    C_OverOp over postfix_expression.

unary_operator:
    OP4;
    '~';
    '*'.

C_OverOp:
C_MultOper;
C_AddOper.

cast_expression:
unary_expression;
'(' type_name ')' cast_expression.

range_expression:
cast_expression;
range_expression C_RangeOper cast_expression.

C_RangeOper:
'..'.

multiplicative_expression:
range_expression;
multiplicative_expression C_MultOper range_expression.

C_MultOper:
OP5;
'*'.

additive_expression:
multiplicative_expression;
additive_expression C_AddOper multiplicative_expression.

C_AddOper:
OP4.

shift_expression:
additive_expression;
shift_expression C_ShiftOper additive_expression.

C_ShiftOper:
OPSHIFT.

relational_expression:
    shift_expression;
    relational_expression C_RelationalOper shift_expression;
    relational_expression C_InOper shift_expression;
    relational_expression holds IDENTIFIER.

C_InOper:
in;
'!' in.

C_RelationalOper:
    '<';
    '>';
    OPLEGE.

equality_expression:
relational_expression;
equality_expression C_EqualityOper relational_expression.

C_EqualityOper:
'==';
'!='.

and_expression:
equality_expression;
and_expression C_BitAndOper equality_expression.

c_bitandoper:
'&'.

exclusive_or_expression:
and_expression;
exclusive_or_expression C_BitXorOper and_expression.

C_BitXorOper:
'^'.

inclusive_or_expression:
exclusive_or_expression;
inclusive_or_expression C_BitOrOper exclusive_or_expression.

C_BitOrOper:
'|'.

logical_and_expression:
inclusive_or_expression;
logical_and_expression C_AndOper inclusive_or_expression.

C_AndOper:
'&&'.

logical_or_expression:
logical_and_expression;
logical_or_expression C_OrOper logical_and_expression.

C_OrOper:
'||'.

ArcImpliesExpression:
logical_or_expression C_ImpliesOper logical_or_expression;
logical_or_expression.

conditional_expression:
ArcImpliesExpression;
ArcImpliesExpression '?' Cexpression ':' conditional_expression.

assignment_expression:
    conditional_expression;
    unary_expression ASSOP assignment_expression;
    unary_expression Assign assignment_expression.

assign:
'='.

cexpression:
    assignment_expression;
    Cexpression ',' assignment_expression;
    ArcExpression.

constant_expression:
conditional_expression.

declaration:
    struct_or_union_or_enum_specifier ';';
    typedef_decl;
    declaration_specifiers init_declarator_list ';';
    ghost '(' declaration_specifiers init_declarator_list ';' ')';
    ghost '(' declaration_specifiers init_declarator_list ')';
    assume '(' spec_predicate_list ')'.

typedef_decl:
typedef specifier_qualifier_list ArcInvariant NewTypeName ';';
typedef specifier_qualifier_list typedef_declarator_list ';'.

declaration_specifiers:
    STORAGECLASS declaration_specifiers;
    inline declaration_specifiers;
    specifier_qualifier_list.

specifier_qualifier_list:
type_qualifier_list declaration_specifiers_3;
declaration_specifiers_3.

declaration_specifiers_3:
type_specifier;
type_specifier type_qualifier_list.

type_specifier:
struct_or_union_or_enum_specifier;
preexisting_type.

preexisting_type:
    TYPEDEF_NAME;
    PREDEFTYPE;
    double_type;
    integral_type.

struct_or_union_or_enum_specifier:
struct_or_union_specifier;
enum_specifier.

integral_type:
    char;
    wchar_t;
    int;
    SIGNMODIFIER;
    SIGNMODIFIER char;
    SIGNMODIFIER int;
    IntLength;
    IntLength SIGNMODIFIER;
    SIGNMODIFIER IntLength;
    IntLength int;
    IntLength SIGNMODIFIER int;
    SIGNMODIFIER IntLength int.

intlength:
    long;
    short;
    long long.

double_type:
double;
long double.

init_declarator_list:
init_declarator;
init_declarator_list ',' init_declarator.

typedef_declarator_list:
typedef_declarator;
typedef_declarator_list ',' typedef_declarator.

init_declarator:
declarator OptPlacement;
declarator OptPlacement '=' initializer.

struct_or_union_specifier:
    STRUCTORUNION IDENTIFIER '{' struct_declaration_list '}';
    STRUCTORUNION '{' struct_declaration_list '}';
    preexisting_struct_or_union_specifier.

preexisting_struct_or_union_specifier:
STRUCTORUNION IDENTIFIER.

struct_declaration_list:
struct_declaration;
struct_declaration_list struct_declaration.

struct_declaration:
    specifier_qualifier_list struct_declarator_list ';';
    ghost '(' specifier_qualifier_list struct_declarator_list ';' ')';
    ghost '(' specifier_qualifier_list struct_declarator_list ')'.

struct_declarator_list:
struct_declarator;
struct_declarator_list ',' struct_declarator.

struct_declarator:
    declarator;
    ':' constant_expression;
    declarator ':' constant_expression.

enum_specifier:
    enum '{' enumerator_list '}';
    enum '{' enumerator_list ',' '}';
    enum IDENTIFIER '{' enumerator_list '}';
    enum IDENTIFIER '{' enumerator_list ',' '}';
    preexisting_enum_specifier.

preexisting_enum_specifier:
enum IDENTIFIER.

enumerator_list:
    IDENTIFIER;
    IDENTIFIER '=' constant_expression;
    enumerator_list ',' IDENTIFIER;
    enumerator_list ',' IDENTIFIER '=' constant_expression.

declarator:
    pointer direct_declarator;
    null pointer direct_declarator;
    direct_declarator;
    null direct_declarator.

typedef_declarator:
    pointer direct_typedef_declarator;
    null pointer direct_typedef_declarator;
    direct_typedef_declarator;
    null direct_typedef_declarator.

direct_declarator:
    IDENTIFIER;
    '(' declarator ')';
    direct_declarator '[' ']';
    direct_declarator '[' ']' null;
    direct_declarator '[' constant_expression ']';
    direct_declarator '[' constant_expression ']' null;
    direct_declarator '(' parameter_type_list ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion;
    direct_declarator '(' ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion.

direct_typedef_declarator:
    NewTypeName;
    TYPEDEF_NAME;
    wchar_t;
    '(' typedef_declarator ')';
    direct_typedef_declarator '[' constant_expression ']';
    direct_typedef_declarator '[' ']';
    direct_typedef_declarator '(' parameter_type_list ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion;
    direct_typedef_declarator '(' ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion.

pointer:
    '*';
    '*' pointer_type_qualifier_list;
    '*' pointer;
    '*' pointer_type_qualifier_list pointer.

type_qualifier_list:
    const;
    volatile;
    type_qualifier_list const;
    type_qualifier_list volatile.

pointer_type_qualifier_list:
    const;
    volatile;
    array;
    null;
    pointer_type_qualifier_list const;
    pointer_type_qualifier_list volatile;
    pointer_type_qualifier_list array;
    pointer_type_qualifier_list null.

parameter_type_list:
parameter_list;
parameter_list ',' '...'.

parameter_list:
parameter_declaration;
parameter_list ',' parameter_declaration.

parameter_declaration:
    specifier_qualifier_list declarator;
    type_name;
    out specifier_qualifier_list declarator;
    out type_name.

named_parameter_list:
named_parameter_declaration;
named_parameter_list ',' named_parameter_declaration.

named_parameter_declaration:
specifier_qualifier_list declarator.

type_name:
specifier_qualifier_list;
specifier_qualifier_list abstract_declarator.

abstract_declarator:
    pointer;
    direct_abstract_declarator;
    pointer direct_abstract_declarator.

direct_abstract_declarator:
    '(' abstract_declarator ')';
    '[' ']';
    '[' ']' null;
    '[' constant_expression ']';
    '[' constant_expression ']' null;
    direct_abstract_declarator '[' ']';
    direct_abstract_declarator '[' ']' null;
    direct_abstract_declarator '[' constant_expression ']';
    direct_abstract_declarator '[' constant_expression ']' null;
    '(' ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion;
    '(' parameter_type_list ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion;
    direct_abstract_declarator '(' ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion;
    direct_abstract_declarator '(' parameter_type_list ')' ArcWrites ArcPrecondition ArcVariant ArcReturns ArcPostAssertion.

initializer:
    assignment_expression;
    '{' initializer_list '}';
    '{' initializer_list ',' '}'.

initializer_list:
initializer;
initializer_list ',' initializer.

statement:
compound_statement;
simple_statement.

simple_statement:
    IDENTIFIER ':' simple_statement;
    expression_statement;
    ArcAssertionStatement;
    jump_statement;
    pass_statement;
    switch_statement;
    if_statement;
    iteration_statement.

simple_statement_no_missing_else:
    IDENTIFIER ':' simple_statement_no_missing_else;
    expression_statement;
    ArcAssertionStatement;
    jump_statement;
    pass_statement;
    switch_statement;
    if_statement_no_missing_else;
    iteration_statement_no_missing_else.

C_Body:
compound_statement;
simple_statement.

C_Body_no_missing_else:
compound_statement;
simple_statement_no_missing_else.

switch_statement:
switch '(' CExpression ')' switch_body.

compound_statement:
ScopeBegin ScopeEnd;
ScopeBegin decl_statement_list ScopeEnd.

decl_statement_list:
    C_DeclStat;
    statement;
    decl_statement_list C_DeclStat;
    decl_statement_list statement.

c_declstat:
declaration.

expression_statement:
real_expression_statement;
';'.

real_expression_statement:
Cexpression ';'.

if_statement:
if '(' CExpression ')' C_Body;
if '(' CExpression ')' C_Body_no_missing_else else C_Body.

if_statement_no_missing_else:
if '(' CExpression ')' C_Body_no_missing_else else C_Body_no_missing_else.

switch_body:
'{' labelled_statements_list '}'.

labelled_statements_list:
    case_labels statement;
    labelled_statements_list statement;
    labelled_statements_list case_labels statement.

case_labels:
    case constant_expression ':';
    case_labels case constant_expression ':';
    default ':';
    case_labels default ':'.

iteration_statement:
    while '(' CExpression ')' ArcLoopHeader C_Body;
    do ArcLoopHeader C_Body while '(' CExpression ')' ';';
    for '(' expression_statement ';' ')' ArcLoopHeader C_Body;
    for '(' expression_statement CExpression ';' ')' ArcLoopHeader C_Body;
    for '(' expression_statement ';' CExpression ')' ArcLoopHeader C_Body;
    for '(' expression_statement CExpression ';' CExpression ')' ArcLoopHeader C_Body.

iteration_statement_no_missing_else:
    while '(' CExpression ')' ArcLoopHeader C_Body_no_missing_else;
    do ArcLoopHeader C_Body while '(' CExpression ')' ';';
    for '(' expression_statement ';' ')' ArcLoopHeader C_Body_no_missing_else;
    for '(' expression_statement CExpression ';' ')' ArcLoopHeader C_Body_no_missing_else;
    for '(' expression_statement ';' CExpression ')' ArcLoopHeader C_Body_no_missing_else;
    for '(' expression_statement CExpression ';' CExpression ')' ArcLoopHeader C_Body_no_missing_else.

jump_statement:
    goto IDENTIFIER ';';
    continue ';';
    break ';';
    return ';';
    return CExpression ';'.

pass_statement:
pass.

translation_unit:
external_declaration;
translation_unit external_declaration.

external_declaration:
    function_definition;
    struct_or_union_or_enum_specifier ';';
    typedef_decl;
    declaration_specifiers init_declarator_list ';';
    ghost '(' declaration_specifiers init_declarator_list ';' ')';
    ghost '(' declaration_specifiers init_declarator_list ')';
    GlobalAssumption;
    GlobalAssertion.

function_definition:
declaration_specifiers declarator compound_statement.

GlobalAssumption:
assume '(' spec_predicate_list ')';
assume '(' '(' named_parameter_list ')' ':' spec_predicate_list ')'.

GlobalAssertion:
assert '(' spec_predicate_list ')';
assert '(' '(' named_parameter_list ')' ':' spec_predicate_list ')'.

spec_expression:
conditional_expression;
ArcExpression.

spec_expression_list:
spec_expression;
spec_expression_list ';' spec_expression.

spec_predicate_list:
spec_expression;
spec_predicate_list ';' spec_expression.

ArcPrecondition:
pre '(' spec_predicate_list ')' ArcPrecondition;
Empty.

ArcAssertionStatement:
assert '(' spec_predicate_list ')' ';'.

ArcReturns:
returns '(' spec_expression ')';
Empty.

ArcPostassertion:
post '(' spec_predicate_list ')' ArcPostAssertion;
Empty.

ArcInvariant:
INVARIANT '(' spec_predicate_list ')'.

ArcWrites:
    writes '(' writes_expression_list ')' ArcWrites;
    writes '(' ')' ArcWrites;
    Empty.

writes_expression_list:
    unary_expression;
    volatile;
    writes_expression_list ';' unary_expression;
    writes_expression_list ';' volatile.

ArcLoopHeader:
ArcWrites ArcKeep ArcVariant.

ArcKeep:
keep '(' spec_predicate_list ')' ArcKeep;
Empty.

ArcVariant:
decrease '(' spec_expression_list')' ArcVariant;
Empty.

--eCv additional expression types
ArcExpression:
    THATorANY ArcBoundVariableDeclaration ':-' conditional_expression;
    those ArcBoundVariableDeclaration ':-' conditional_expression;
    forall ArcBoundVariableDeclarations ':-' conditional_expression;
    exists ArcBoundVariableDeclarations ':-' conditional_expression;
    for thoseArcBoundVariableDeclaration ':-' conditional_expression yield conditional_expression;
    for ArcBoundVariableDeclaration yield conditional_expression.

ArcBoundVariableDeclarations:
ArcBoundVariableDeclaration;
ArcBoundVariableDeclarations ';' ArcBoundVariableDeclaration.

ArcBoundVariableDeclaration:
specifier_qualifier_list declarator;
IDENTIFIER in shift_expression.

C_ImpliesOper:
'=>'.

ScopeBegin:
'{'.

ScopeEnd:
'}'.

NewTypeName:
IDENTIFIER.

-- String concatenation (when not handled by the preprocessor)
c_stringliteral:
    EMPTYSTRINGLITERAL;
    NONEMPTYSTRINGLITERAL;
    c_stringLiteral EMPTYSTRINGLITERAL;
    c_stringLiteral NONEMPTYSTRINGLITERAL.

-- Extension for some C compilers for embedded processors
OptPlacement:
'@' conditional_expression;
Empty.

TOC