Grammar railroad diagram #897

mingodad · 2025-03-02T15:02:14Z

I've just added the core grammar to https://mingodad.github.io/parsertl-playground/playground/ an Yacc/Lex like online interpreter/editor (select Cerberus-core parser (partially working) from Examples then click Parse to see a parse tree for the content in Input source) and from there generated an EBNF understood by https://github.com/GuntherRademacher/rr that generates a nice navigable railroad diagram (see bellow with instructions at the top).

Notice that I replaced right recursion by left recursion !!

//
// EBNF to be viewd at
//    (IPV6) https://www.bottlecaps.de/rr/ui
//    (IPV4) https://rr.red-dove.com/ui
//
// Copy and paste this at one of the urls shown above in the 'Edit Grammar' tab
// then click the 'View Diagram' tab.
//

start::=
	  nonempty_list_declaration_

attribute::=
	  LBRACKET loption_separated_nonempty_list_COMMA_attribute_pair__ RBRACKET

attribute_pair::=
	  AILNAME EQ CSTRING

integer_base_type::=
	  ICHAR
	| SHORT
	| INT
	| LONG
	| LONG_LONG

integer_type::=
	  CHAR
	| BOOL
	| INT8_T
	| INT16_T
	| INT32_T
	| INT64_T
	| UINT8_T
	| UINT16_T
	| UINT32_T
	| UINT64_T
	| INTMAX_T
	| INTPTR_T
	| UINTMAX_T
	| UINTPTR_T
	| SIGNED integer_base_type
	| UNSIGNED integer_base_type
	| SIZE_T
	| PTRDIFF_T

floating_type::=
	  FLOAT
	| DOUBLE
	| LONG_DOUBLE

basic_type::=
	  integer_type
	| floating_type

ctype::=
	  VOID
	| basic_type
	| ctype LBRACKET option_INT_CONST_ RBRACKET
	| ctype LPAREN params RPAREN
	| CONST ctype STAR
	| ctype STAR
	| ATOMIC LPAREN ctype RPAREN
	| SYM
	| STRUCT SYM
	| UNION SYM

params::=
	  loption_separated_nonempty_list_COMMA_ctype__
	| loption_separated_nonempty_list_COMMA_ctype__ COMMA DOTS

core_object_type::=
	  INTEGER
	| FLOATING
	| POINTER
	| ARRAY LPAREN core_object_type RPAREN
	| STRUCT SYM
	| UNION SYM

core_base_type::=
	  UNIT
	| BOOLEAN
	| CTYPE
	| LBRACKET core_base_type RBRACKET
	| LPAREN loption_separated_nonempty_list_COMMA_core_base_type__ RPAREN
	| core_object_type
	| LOADED core_object_type
	| STORABLE

core_type::=
	  core_base_type
	| EFF core_base_type

name::=
	  SYM
	| IMPL

cabs_id::=
	  SYM

memory_order::=
	  SEQ_CST
	| RELAXED
	| RELEASE
	| ACQUIRE
	| CONSUME
	| ACQ_REL

ctor::=
	  ARRAYCTOR
	| IVMAX
	| IVMIN
	| IVSIZEOF
	| IVALIGNOF
	| SPECIFIED
	| UNSPECIFIED
	| FVFROMINT
	| IVFROMFLOAT
	| IVCOMPL
	| IVAND
	| IVOR
	| IVXOR

list_pattern::=
	  BRACKETS COLON core_base_type
	| pattern COLON_COLON pattern
	| LBRACKET loption_separated_nonempty_list_COMMA_pattern__ RBRACKET COLON core_base_type

pattern::=
	  SYM COLON core_base_type
	| UNDERSCORE COLON core_base_type
	| list_pattern
	| LPAREN pattern COMMA separated_nonempty_list_COMMA_pattern_ RPAREN
	| ctor LPAREN loption_separated_nonempty_list_COMMA_pattern__ RPAREN

pattern_pair_expr_::=
	  PIPE pattern EQ_GT expr

pattern_pair_pexpr_::=
	  PIPE pattern EQ_GT pexpr

core_ctype::=
	  SQUOTE ctype SQUOTE

core_integer_type::=
	  SQUOTE integer_type SQUOTE

value::=
	  INT_CONST
	| IVMAX_ALIGNMENT
	| NULL LPAREN ctype RPAREN
	| CFUNCTION_VALUE LPAREN name RPAREN
	| UNIT_VALUE
	| TRUE
	| FALSE
	| core_ctype

list_pexpr::=
	  BRACKETS COLON core_base_type
	| pexpr COLON_COLON pexpr
	| LBRACKET loption_separated_nonempty_list_COMMA_pexpr__ RBRACKET COLON core_base_type

member::=
	  DOT cabs_id EQ pexpr

pexpr::=
	  LPAREN pexpr RPAREN
	| UNDEF LPAREN UB RPAREN
	| ERROR LPAREN STRING COMMA pexpr RPAREN
	| value
	| SYM
	| IMPL
	| LPAREN pexpr COMMA separated_nonempty_list_COMMA_pexpr_ RPAREN
	| list_pexpr
	| ctor LPAREN loption_separated_nonempty_list_COMMA_pexpr__ RPAREN
	| CASE pexpr OF list_pattern_pair_pexpr__ END
	| ARRAY_SHIFT LPAREN pexpr COMMA core_ctype COMMA pexpr RPAREN
	| MEMBER_SHIFT LPAREN pexpr COMMA SYM COMMA DOT cabs_id RPAREN
	| NOT LPAREN pexpr RPAREN
	| MINUS pexpr
	| CFUNCTION LPAREN pexpr RPAREN
	| pexpr PLUS pexpr
	| pexpr MINUS pexpr
	| pexpr STAR pexpr
	| pexpr SLASH pexpr
	| pexpr REM_T pexpr
	| pexpr REM_F pexpr
	| pexpr CARET pexpr
	| pexpr EQ pexpr
	| pexpr GT pexpr
	| pexpr LT pexpr
	| pexpr GE pexpr
	| pexpr LE pexpr
	| pexpr SLASH_BACKSLASH pexpr
	| pexpr BACKSLASH_SLASH pexpr
	| CONV_INT LPAREN core_integer_type COMMA pexpr RPAREN
	| WRAPI LPAREN core_integer_type COMMA pexpr COMMA pexpr RPAREN
	| CATCH_EXCEPTIONAL_CONDITION LPAREN core_integer_type COMMA pexpr COMMA pexpr RPAREN
	| MEMOP LPAREN PURE_MEMOP_OP COMMA loption_separated_nonempty_list_COMMA_pexpr__ RPAREN
	| LPAREN STRUCT SYM RPAREN LBRACE loption_separated_nonempty_list_COMMA_member__ RBRACE
	| LPAREN UNION SYM RPAREN LBRACE member RBRACE
	| name LPAREN loption_separated_nonempty_list_COMMA_pexpr__ RPAREN
	| LET pattern EQ pexpr IN pexpr
	| IF pexpr THEN pexpr ELSE pexpr
	| IS_SCALAR LPAREN pexpr RPAREN
	| IS_INTEGER LPAREN pexpr RPAREN
	| IS_SIGNED LPAREN pexpr RPAREN
	| IS_UNSIGNED LPAREN pexpr RPAREN
	| ARE_COMPATIBLE LPAREN pexpr COMMA pexpr RPAREN
	| BRACKETS

memop_op::=
	  MEMOP_OP
	| PTRMEMBERSHIFT LBRACKET SYM COMMA DOT cabs_id RBRACKET

expr::=
	  LPAREN expr RPAREN
	| PURE LPAREN pexpr RPAREN
	| MEMOP LPAREN memop_op COMMA loption_separated_nonempty_list_COMMA_pexpr__ RPAREN
	| LET pattern EQ pexpr IN expr
	| IF pexpr THEN expr ELSE expr
	| CASE pexpr OF list_pattern_pair_expr__ END
	| PCALL LPAREN name RPAREN
	| PCALL LPAREN name COMMA separated_nonempty_list_COMMA_pexpr_ RPAREN
	| CCALL LPAREN pexpr COMMA pexpr RPAREN
	| CCALL LPAREN pexpr COMMA pexpr COMMA separated_nonempty_list_COMMA_pexpr_ RPAREN
	| paction
	| UNSEQ LPAREN loption_separated_nonempty_list_COMMA_expr__ RPAREN
	| LET WEAK pattern EQ expr IN expr
	| expr SEMICOLON expr
	| LET STRONG pattern EQ expr IN expr
	| BOUND LPAREN expr RPAREN
	| SAVE SYM COLON core_base_type LPAREN loption_separated_nonempty_list_COMMA_separated_pair_SYM_COLON_separated_pair_core_base_type_COLON_EQ_pexpr____ RPAREN IN expr
	| RUN SYM LPAREN loption_separated_nonempty_list_COMMA_pexpr__ RPAREN
	| ND LPAREN loption_separated_nonempty_list_COMMA_expr__ RPAREN
	| PAR LPAREN loption_separated_nonempty_list_COMMA_expr__ RPAREN

action::=
	  CREATE LPAREN pexpr COMMA pexpr RPAREN
	| CREATE_READONLY LPAREN pexpr COMMA pexpr COMMA pexpr RPAREN
	| ALLOC LPAREN pexpr COMMA pexpr RPAREN
	| FREE LPAREN pexpr RPAREN
	| KILL LPAREN core_ctype COMMA pexpr RPAREN
	| STORE LPAREN pexpr COMMA pexpr COMMA pexpr RPAREN
	| STORE_LOCK LPAREN pexpr COMMA pexpr COMMA pexpr RPAREN
	| LOAD LPAREN pexpr COMMA pexpr RPAREN
	| STORE LPAREN pexpr COMMA pexpr COMMA pexpr COMMA memory_order RPAREN
	| STORE_LOCK LPAREN pexpr COMMA pexpr COMMA pexpr COMMA memory_order RPAREN
	| LOAD LPAREN pexpr COMMA pexpr COMMA memory_order RPAREN
	| SEQ_RMW LPAREN pexpr COMMA pexpr COMMA SYM EQ_GT pexpr RPAREN
	| SEQ_RMW_WITH_FORWARD LPAREN pexpr COMMA pexpr COMMA SYM EQ_GT pexpr RPAREN
	| RMW LPAREN pexpr COMMA pexpr COMMA pexpr COMMA pexpr COMMA memory_order COMMA memory_order RPAREN
	| FENCE LPAREN memory_order RPAREN
	| SKIP

paction::=
	  action
	| NEG LPAREN action RPAREN

def_declaration::=
	  DEF IMPL COLON core_base_type COLON_EQ pexpr

def_field::=
	  cabs_id COLON core_ctype

def_fields::=
	  def_field
	| def_fields def_field

def_aggregate_declaration::=
	  DEF STRUCT SYM COLON_EQ def_fields
	| DEF UNION SYM COLON_EQ def_fields

ifun_declaration::=
	  FUN IMPL LPAREN loption_separated_nonempty_list_COMMA_separated_pair_SYM_COLON_core_base_type___ RPAREN COLON core_base_type COLON_EQ pexpr

glob_ctype_attribute::=
	  LBRACKET AILCTYPE EQ core_ctype RBRACKET

glob_declaration::=
	  GLOB SYM COLON core_type glob_ctype_attribute COLON_EQ expr

fun_declaration::=
	  FUN SYM LPAREN loption_separated_nonempty_list_COMMA_separated_pair_SYM_COLON_core_base_type___ RPAREN COLON core_base_type COLON_EQ pexpr

proc_declaration::=
	  PROC option_attribute_ SYM LPAREN loption_separated_nonempty_list_COMMA_separated_pair_SYM_COLON_core_base_type___ RPAREN COLON EFF core_base_type COLON_EQ expr

builtin_declaration::=
	  BUILTIN SYM LPAREN loption_separated_nonempty_list_COMMA_core_base_type__ RPAREN COLON EFF core_base_type

declaration::=
	  def_declaration
	| ifun_declaration
	| glob_declaration
	| fun_declaration
	| proc_declaration
	| builtin_declaration
	| def_aggregate_declaration

option_INT_CONST_::=
	  /*%empty*/
	| INT_CONST

option_attribute_::=
	  /*%empty*/
	| attribute

loption_separated_nonempty_list_COMMA_attribute_pair__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_attribute_pair_

loption_separated_nonempty_list_COMMA_core_base_type__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_core_base_type_

loption_separated_nonempty_list_COMMA_ctype__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_ctype_

loption_separated_nonempty_list_COMMA_expr__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_expr_

loption_separated_nonempty_list_COMMA_member__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_member_

loption_separated_nonempty_list_COMMA_pattern__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_pattern_

loption_separated_nonempty_list_COMMA_pexpr__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_pexpr_

loption_separated_nonempty_list_COMMA_separated_pair_SYM_COLON_core_base_type___::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_separated_pair_SYM_COLON_core_base_type__

loption_separated_nonempty_list_COMMA_separated_pair_SYM_COLON_separated_pair_core_base_type_COLON_EQ_pexpr____::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_separated_pair_SYM_COLON_separated_pair_core_base_type_COLON_EQ_pexpr___

list_pattern_pair_expr__::=
	  /*%empty*/
	| pattern_pair_expr_ list_pattern_pair_expr__

list_pattern_pair_pexpr__::=
	  /*%empty*/
	| pattern_pair_pexpr_ list_pattern_pair_pexpr__

nonempty_list_declaration_::=
	  declaration
	| nonempty_list_declaration_ declaration

separated_nonempty_list_COMMA_attribute_pair_::=
	  attribute_pair
	| separated_nonempty_list_COMMA_attribute_pair_ COMMA attribute_pair

separated_nonempty_list_COMMA_core_base_type_::=
	  core_base_type
	| separated_nonempty_list_COMMA_core_base_type_ COMMA core_base_type

separated_nonempty_list_COMMA_ctype_::=
	  ctype
	| separated_nonempty_list_COMMA_ctype_ COMMA ctype

separated_nonempty_list_COMMA_expr_::=
	  expr
	| separated_nonempty_list_COMMA_expr_ COMMA expr

separated_nonempty_list_COMMA_member_::=
	  member
	| separated_nonempty_list_COMMA_member_ COMMA member

separated_nonempty_list_COMMA_pattern_::=
	  pattern
	| separated_nonempty_list_COMMA_pattern_ COMMA pattern

separated_nonempty_list_COMMA_pexpr_::=
	  pexpr
	| separated_nonempty_list_COMMA_pexpr_ COMMA pexpr

separated_nonempty_list_COMMA_separated_pair_SYM_COLON_core_base_type__::=
	  SYM COLON core_base_type
	| separated_nonempty_list_COMMA_separated_pair_SYM_COLON_core_base_type__ COMMA SYM COLON core_base_type

separated_nonempty_list_COMMA_separated_pair_SYM_COLON_separated_pair_core_base_type_COLON_EQ_pexpr___::=
	  SYM COLON core_base_type COLON_EQ pexpr
	| separated_nonempty_list_COMMA_separated_pair_SYM_COLON_separated_pair_core_base_type_COLON_EQ_pexpr___ COMMA SYM COLON core_base_type COLON_EQ pexpr

//Tokens

BACKSLASH_SLASH ::= "\\/"
BRACKETS ::= "[]"
CARET ::= "^"
COLON ::= ":"
COLON_COLON ::= "::"
COLON_EQ ::= ":="
COMMA ::= ","
DOT ::= "."
DOTS ::= "..."
EQ ::= "="
EQ_GT ::= "=>"
GE ::= ">="
GT ::= ">"
LBRACE ::= "{"
LBRACKET ::= "["
LE ::= "<="
LPAREN ::= "("
LT ::= "<"
MINUS ::= "-"
NEG ::= "neg"
PIPE ::= "|"
PLUS ::= "+"
PURE_MEMOP_OP ::= "PURE_MEMOP_OP"
RBRACE ::= "}"
RBRACKET ::= "]"
REM_F ::= "rem_f"
REM_T ::= "rem_t"
RPAREN ::= ")"
SEMICOLON ::= ";"
SLASH ::= "/"
SLASH_BACKSLASH ::= "/\\"
SQUOTE ::= "'"
STAR ::= "*"
UNDERSCORE ::= "_"

/* for Core ctypes */
CONST ::= "const"
ATOMIC ::= "_Atomic"
BOOL ::= "_Bool"
CHAR ::= "char"
DOUBLE ::= "double"
/* ENUM ::= "enum"               */
FLOAT ::= "float"
INT ::= "int"
ICHAR ::= "ichar"
LONG ::= "long"
LONG_DOUBLE ::= "long_double"
LONG_LONG ::= "long_long"
SHORT ::= "short"
SIGNED ::= "signed"
STRUCT ::= "struct"
UNION ::= "union"
UNSIGNED ::= "unsigned"
VOID ::= "void"
INT8_T ::= "int8_t"
INT16_T ::= "int16_t"
INT32_T ::= "int32_t"
INT64_T ::= "int64_t"
UINT8_T ::= "uint8_t"
UINT16_T ::= "uint16_t"
UINT32_T ::= "uint32_t"
UINT64_T ::= "uint64_t"
INTPTR_T ::= "intptr_t"
INTMAX_T ::= "intmax_t"
UINTPTR_T ::= "uintptr_t"
UINTMAX_T ::= "uintmax_t"
SIZE_T ::= "size_t"
PTRDIFF_T ::= "ptrdiff_t"

/* for Core object types */
INTEGER ::= "integer"
FLOATING ::= "floating"
POINTER ::= "pointer"
ARRAY ::= "array"
CFUNCTION ::= "cfunction"

/* for Core base types */
UNIT ::= "unit"
BOOLEAN ::= "boolean"
CTYPE ::= "ctype"
LOADED ::= "loaded"
STORABLE ::= "storable"

/* for Core types */
EFF ::= "eff"

/* for Core values */
NULL ::= "NULL"
UNIT_VALUE ::= "Unit"
TRUE ::= "True"
FALSE ::= "False"
IVMAX ::= "Ivmax"
IVMIN ::= "Ivmin"
IVSIZEOF ::= "Ivsizeof"
IVALIGNOF ::= "Ivalignof"
IVCOMPL ::= "IvCOMPL"
IVAND ::= "IvAND"
IVOR ::= "IvOR"
IVXOR ::= "IvXOR"
SPECIFIED ::= "Specified"
UNSPECIFIED ::= "Unspecified"
CFUNCTION_VALUE ::= "Cfunction"
ARRAYCTOR ::= "Array"

FVFROMINT ::= "Fvfromint"
IVFROMFLOAT ::= "Ivfromfloat"

/* this is a fake constructor at the syntax level */
/* NOTE: it would be better to pass to the Core parser an env with the C types symbols (to resolve max_align_t) */
IVMAX_ALIGNMENT ::= "IvMaxAlignment"

/* for Core (pure) expressions */
NOT ::= "not"
UNDEF ::= "undef"
ERROR ::= "error"
LET ::= "let"
IN ::= "in"
IF ::= "if"
THEN ::= "then"
ELSE ::= "else"
PURE ::= "pure"
UNSEQ ::= "unseq"
WEAK ::= "weak"
STRONG ::= "strong"
SAVE ::= "save"
RUN ::= "run"
BOUND ::= "bound"
ND ::= "nd"
PAR ::= "par"
ARRAY_SHIFT ::= "array_shift"
MEMBER_SHIFT ::= "member_shift"
CASE ::= "case"
OF ::= "of"
END ::= "end"
PCALL ::= "pcall"
CCALL ::= "ccall"
MEMOP ::= "memop"

/* Core (pure) builtins for bounded intger arithmetic */
CONV_INT ::= "__conv_int__"
WRAPI ::= "wrapI_add"
WRAPI ::= "wrapI_sub"
WRAPI ::= "wrapI_mul"
WRAPI ::= "wrapI_shl"
WRAPI ::= "wrapI_shr"
CATCH_EXCEPTIONAL_CONDITION ::= "catch_exceptional_condition_add"
CATCH_EXCEPTIONAL_CONDITION ::= "catch_exceptional_condition_sub"
CATCH_EXCEPTIONAL_CONDITION ::= "catch_exceptional_condition_mul"
CATCH_EXCEPTIONAL_CONDITION ::= "catch_exceptional_condition_shl"
CATCH_EXCEPTIONAL_CONDITION ::= "catch_exceptional_condition_shr"

/* for Core.action_ */
CREATE ::= "create"
CREATE_READONLY ::= "create_readonly"
ALLOC ::= "alloc"
FREE ::= "free"
KILL ::= "kill"
STORE ::= "store"
STORE_LOCK ::= "store_lock"
LOAD ::= "load"
SEQ_RMW ::= "seq_rmw"
SEQ_RMW_WITH_FORWARD ::= "seq_rmw_with_forward"
RMW ::= "rmw"
FENCE ::= "fence"
/*      "compare_exchange_strong"  COMPARE_EXCHANGE_STRONG */

/* for toplevel declarations */
DEF ::= "def" /* for implementation files only */
GLOB ::= "glob"
FUN ::= "fun"
PROC ::= "proc"

/* for C11 memory orders */
SEQ_CST ::= "seq_cst"
RELAXED ::= "relaxed"
RELEASE ::= "release"
ACQUIRE ::= "acquire"
CONSUME ::= "consume"
ACQ_REL ::= "acq_rel"

/* TODO: temporary */
IS_SCALAR ::= "is_scalar"
IS_INTEGER ::= "is_integer"
IS_SIGNED ::= "is_signed"
IS_UNSIGNED ::= "is_unsigned"
ARE_COMPATIBLE ::= "are_compatible"

/* for Memory operations */
MEMOP_OP ::= "PtrEq"
MEMOP_OP ::= "PtrNe"
MEMOP_OP ::= "PtrLt"
MEMOP_OP ::= "PtrGt"
MEMOP_OP ::= "PtrLe"
MEMOP_OP ::= "PtrGe"
MEMOP_OP ::= "Ptrdiff"
MEMOP_OP ::= "IntFromPtr"
MEMOP_OP ::= "PtrFromInt"
MEMOP_OP ::= "PtrValidForDeref"
MEMOP_OP ::= "PtrWellAligned"
MEMOP_OP ::= "PtrArrayShift"
PTRMEMBERSHIFT ::= "PtrMemberShift"

MEMOP_OP ::= "Memcpy"
MEMOP_OP ::= "Memcmp"
MEMOP_OP ::= "Realloc"
MEMOP_OP ::= "Va_start"
MEMOP_OP ::= "Va_copy"
MEMOP_OP ::= "Va_arg"
MEMOP_OP ::= "Va_end"
MEMOP_OP ::= "Copy_alloc_id"

/* for source attributes */
AILNAME ::= "ailname"

AILCTYPE ::= "ail_ctype"

/* for core builtins */
BUILTIN ::= "builtin"

SKIP ::= "skip" //missing ?

The text was updated successfully, but these errors were encountered:

mingodad · 2025-03-02T15:35:58Z

And here is a partial EBNF from the C grammar (missing several cn_* rules).

//
// EBNF to be viewd at
//    (IPV6) https://www.bottlecaps.de/rr/ui
//    (IPV4) https://rr.red-dove.com/ui
//
// Copy and paste this at one of the urls shown above in the 'Edit Grammar' tab
// then click the 'View Diagram' tab.
//

translation_unit::=
	  EOF
	| external_declaration_list EOF

list_eq1_TYPEDEF_declaration_specifier_::=
	  TYPEDEF list_declaration_specifier_
	| declaration_specifier list_eq1_TYPEDEF_declaration_specifier_

list_eq1_attribute_type_specifier_unique_declaration_specifier_::=
	  attribute_type_specifier_unique list_declaration_specifier_
	| declaration_specifier list_eq1_attribute_type_specifier_unique_declaration_specifier_

list_ge1_attribute_type_specifier_nonunique_declaration_specifier_::=
	  attribute_type_specifier_nonunique list_declaration_specifier_
	| attribute_type_specifier_nonunique list_ge1_attribute_type_specifier_nonunique_declaration_specifier_
	| declaration_specifier list_ge1_attribute_type_specifier_nonunique_declaration_specifier_

list_eq1_eq1_TYPEDEF_attribute_type_specifier_unique_declaration_specifier_::=
	  TYPEDEF list_eq1_attribute_type_specifier_unique_declaration_specifier_
	| attribute_type_specifier_unique list_eq1_TYPEDEF_declaration_specifier_
	| declaration_specifier list_eq1_eq1_TYPEDEF_attribute_type_specifier_unique_declaration_specifier_

list_eq1_ge1_TYPEDEF_attribute_type_specifier_nonunique_declaration_specifier_::=
	  TYPEDEF list_ge1_attribute_type_specifier_nonunique_declaration_specifier_
	| attribute_type_specifier_nonunique list_eq1_TYPEDEF_declaration_specifier_
	| attribute_type_specifier_nonunique list_eq1_ge1_TYPEDEF_attribute_type_specifier_nonunique_declaration_specifier_
	| declaration_specifier list_eq1_ge1_TYPEDEF_attribute_type_specifier_nonunique_declaration_specifier_

list_pair_attribute_type_qualifier_attribute_alignment_specifier_::=
	  /*%empty*/
	| attribute_type_qualifier list_pair_attribute_type_qualifier_attribute_alignment_specifier_
	| attribute_alignment_specifier list_pair_attribute_type_qualifier_attribute_alignment_specifier_

list_tuple3_eq1_attribute_type_specifier_unique_attribute_type_qualifier_attribute_alignment_specifier_::=
	  attribute_type_specifier_unique list_pair_attribute_type_qualifier_attribute_alignment_specifier_
	| attribute_type_qualifier list_tuple3_eq1_attribute_type_specifier_unique_attribute_type_qualifier_attribute_alignment_specifier_
	| attribute_alignment_specifier list_tuple3_eq1_attribute_type_specifier_unique_attribute_type_qualifier_attribute_alignment_specifier_

list_tuple3_ge1_attribute_type_specifier_nonunique_attribute_type_qualifier_attribute_alignment_specifier_::=
	  attribute_type_specifier_nonunique list_pair_attribute_type_qualifier_attribute_alignment_specifier_
	| attribute_type_specifier_nonunique list_tuple3_ge1_attribute_type_specifier_nonunique_attribute_type_qualifier_attribute_alignment_specifier_
	| attribute_type_qualifier list_tuple3_ge1_attribute_type_specifier_nonunique_attribute_type_qualifier_attribute_alignment_specifier_
	| attribute_alignment_specifier list_tuple3_ge1_attribute_type_specifier_nonunique_attribute_type_qualifier_attribute_alignment_specifier_

typedef_name::=
	  UNAME TYPE
	| LNAME TYPE

var_name::=
	  UNAME VARIABLE
	| LNAME VARIABLE

typedef_name_spec::=
	  typedef_name

general_identifier::=
	  typedef_name
	| var_name

save_context::=
	  /*%empty*/

scoped_compound_statement_::=
	  save_context compound_statement

scoped_iteration_statement_::=
	  save_context iteration_statement

scoped_parameter_type_list_::=
	  save_context parameter_type_list

scoped_selection_statement_::=
	  save_context selection_statement

scoped_statement_::=
	  save_context statement

declarator_varname::=
	  declarator

declarator_typedefname::=
	  declarator

enumeration_constant::=
	  general_identifier

primary_expression::=
	  var_name
	| CONSTANT
	| string_literal
	| LPAREN expression RPAREN
	| generic_selection
	| LPAREN LBRACE option_block_item_list_ RBRACE RPAREN

generic_selection::=
	  GENERIC LPAREN assignment_expression COMMA generic_assoc_list RPAREN

generic_assoc_list::=
	  generic_association
	| generic_assoc_list COMMA generic_association

generic_association::=
	  type_name COLON assignment_expression
	| DEFAULT COLON assignment_expression

postfix_expression::=
	  primary_expression
	| postfix_expression LBRACK expression RBRACK
	| postfix_expression LPAREN option_argument_expression_list_ RPAREN
	| postfix_expression DOT general_identifier
	| postfix_expression MINUS_GT general_identifier
	| postfix_expression PLUS_PLUS
	| postfix_expression MINUS_MINUS
	| LPAREN type_name RPAREN LBRACE initializer_list option_COMMA_ RBRACE
	| ASSERT LPAREN assignment_expression RPAREN
	| VA_START LPAREN assignment_expression COMMA general_identifier RPAREN
	| VA_COPY LPAREN assignment_expression COMMA assignment_expression RPAREN
	| VA_ARG LPAREN assignment_expression COMMA type_name RPAREN
	| VA_END LPAREN assignment_expression RPAREN
	| OFFSETOF LPAREN type_name COMMA general_identifier RPAREN
	| BUILTIN_TYPES_COMPATIBLE_P LPAREN type_name COMMA type_name RPAREN
	| BUILTIN_CHOOSE_EXPR LPAREN assignment_expression COMMA assignment_expression COMMA assignment_expression RPAREN
	| PRINT_TYPE LPAREN expression RPAREN
	| BMC_ASSUME LPAREN assignment_expression RPAREN

argument_expression_list::=
	  assignment_expression
	| argument_expression_list COMMA assignment_expression

unary_expression::=
	  postfix_expression
	| PLUS_PLUS unary_expression
	| MINUS_MINUS unary_expression
	| unary_operator cast_expression
	| SIZEOF unary_expression
	| SIZEOF LPAREN type_name RPAREN
	| ALIGNOF LPAREN type_name RPAREN

unary_operator::=
	  AMPERSAND
	| STAR
	| PLUS
	| MINUS
	| TILDE
	| BANG

cast_expression::=
	  unary_expression
	| LPAREN type_name RPAREN cast_expression

multiplicative_expression::=
	  cast_expression
	| multiplicative_expression STAR cast_expression
	| multiplicative_expression SLASH cast_expression
	| multiplicative_expression PERCENT cast_expression

additive_expression::=
	  multiplicative_expression
	| additive_expression PLUS multiplicative_expression
	| additive_expression MINUS multiplicative_expression

shift_expression::=
	  additive_expression
	| shift_expression LT_LT additive_expression
	| shift_expression GT_GT additive_expression

relational_expression::=
	  shift_expression
	| relational_expression LT shift_expression
	| relational_expression GT shift_expression
	| relational_expression LT_EQ shift_expression
	| relational_expression GT_EQ shift_expression

equality_expression::=
	  relational_expression
	| equality_expression EQ_EQ relational_expression
	| equality_expression BANG_EQ relational_expression

_AND_expression::=
	  equality_expression
	| _AND_expression AMPERSAND equality_expression

exclusive_OR_expression::=
	  _AND_expression
	| exclusive_OR_expression CARET _AND_expression

inclusive_OR_expression::=
	  exclusive_OR_expression
	| inclusive_OR_expression PIPE exclusive_OR_expression

logical_AND_expression::=
	  inclusive_OR_expression
	| logical_AND_expression AMPERSAND_AMPERSAND inclusive_OR_expression

logical_OR_expression::=
	  logical_AND_expression
	| logical_OR_expression PIPE_PIPE logical_AND_expression

conditional_expression::=
	  logical_OR_expression
	| logical_OR_expression QUESTION expression COLON conditional_expression
	| logical_OR_expression QUESTION_COLON conditional_expression

assignment_expression::=
	  conditional_expression
	| unary_expression assignment_operator assignment_expression

assignment_operator::=
	  EQ
	| STAR_EQ
	| SLASH_EQ
	| PERCENT_EQ
	| PLUS_EQ
	| MINUS_EQ
	| LT_LT_EQ
	| GT_GT_EQ
	| AMPERSAND_EQ
	| CARET_EQ
	| PIPE_EQ

expression::=
	  assignment_expression
	| expression COMMA assignment_expression

constant_expression::=
	  conditional_expression

no_leading_attribute_declaration::=
	  declaration_specifiers option_init_declarator_list_declarator_varname__ SEMICOLON
	| declaration_specifiers_typedef option_init_declarator_list_declarator_typedefname__ SEMICOLON
	| static_assert_declaration

declaration::=
	  no_leading_attribute_declaration
	| attribute_specifier_sequence declaration_specifiers option_init_declarator_list_declarator_varname__ SEMICOLON
	| attribute_specifier_sequence declaration_specifiers_typedef option_init_declarator_list_declarator_typedefname__ SEMICOLON
	| attribute_declaration

declaration_specifier::=
	  storage_class_specifier
	| storage_class_specifier attribute_specifier_sequence
	| type_qualifier
	| type_qualifier attribute_specifier_sequence
	| function_specifier
	| function_specifier attribute_specifier_sequence
	| alignment_specifier
	| alignment_specifier attribute_specifier_sequence

declaration_specifiers::=
	  list_eq1_attribute_type_specifier_unique_declaration_specifier_
	| list_ge1_attribute_type_specifier_nonunique_declaration_specifier_

declaration_specifiers_typedef::=
	  list_eq1_eq1_TYPEDEF_attribute_type_specifier_unique_declaration_specifier_
	| list_eq1_ge1_TYPEDEF_attribute_type_specifier_nonunique_declaration_specifier_

init_declarator_list_declarator_typedefname_::=
	  init_declarator_declarator_typedefname_
	| init_declarator_list_declarator_typedefname_ COMMA init_declarator_declarator_typedefname_

init_declarator_list_declarator_varname_::=
	  init_declarator_declarator_varname_
	| init_declarator_list_declarator_varname_ COMMA init_declarator_declarator_varname_

init_declarator_declarator_typedefname_::=
	  declarator_typedefname
	| declarator_typedefname asm_register
	| declarator_typedefname EQ initializer_
	| declarator_typedefname asm_register EQ initializer_

init_declarator_declarator_varname_::=
	  declarator_varname
	| declarator_varname asm_register
	| declarator_varname EQ initializer_
	| declarator_varname asm_register EQ initializer_

storage_class_specifier::=
	  EXTERN
	| STATIC
	| THREAD_LOCAL
	| AUTO
	| REGISTER

type_specifier_nonunique::=
	  CHAR
	| SHORT
	| INT
	| LONG
	| FLOAT
	| DOUBLE
	| SIGNED
	| UNSIGNED
	| COMPLEX

attribute_type_specifier_nonunique::=
	  type_specifier_nonunique
	| type_specifier_nonunique attribute_specifier_sequence

type_specifier_unique::=
	  VOID
	| BOOL
	| atomic_type_specifier
	| struct_or_union_specifier
	| enum_specifier
	| typedef_name_spec
	| TYPEOF LPAREN expression RPAREN
	| TYPEOF LPAREN type_name RPAREN

attribute_type_specifier_unique::=
	  type_specifier_unique
	| type_specifier_unique attribute_specifier_sequence

struct_or_union_specifier::=
	  struct_or_union option_attribute_specifier_sequence_ option_general_identifier_ LBRACE boption_nonempty_list_SEMICOLON__ struct_declaration_list RBRACE
	| struct_or_union option_attribute_specifier_sequence_ general_identifier
	| struct_or_union option_attribute_specifier_sequence_ option_general_identifier_ LBRACE RBRACE

struct_or_union::=
	  STRUCT
	| UNION

struct_declaration_list::=
	  struct_declaration
	| struct_declaration_list struct_declaration

struct_declaration::=
	  specifier_qualifier_list option_struct_declarator_list_ SEMICOLON boption_nonempty_list_SEMICOLON__
	| attribute_specifier_sequence specifier_qualifier_list option_struct_declarator_list_ SEMICOLON boption_nonempty_list_SEMICOLON__
	| static_assert_declaration

specifier_qualifier_list::=
	  list_tuple3_eq1_attribute_type_specifier_unique_attribute_type_qualifier_attribute_alignment_specifier_
	| list_tuple3_ge1_attribute_type_specifier_nonunique_attribute_type_qualifier_attribute_alignment_specifier_

struct_declarator_list::=
	  struct_declarator
	| struct_declarator_list COMMA struct_declarator

struct_declarator::=
	  declarator
	| option_declarator_ COLON constant_expression

enum_specifier::=
	  ENUM option_general_identifier_ LBRACE enumerator_list option_COMMA_ RBRACE
	| ENUM attribute_specifier_sequence option_general_identifier_ LBRACE enumerator_list option_COMMA_ RBRACE
	| ENUM general_identifier
	| ENUM attribute_specifier_sequence general_identifier

enumerator_list::=
	  enumerator
	| enumerator_list COMMA enumerator

enumerator::=
	  enumeration_constant
	| enumeration_constant attribute_specifier_sequence
	| enumeration_constant EQ constant_expression
	| enumeration_constant attribute_specifier_sequence EQ constant_expression

atomic_type_specifier::=
	  ATOMIC LPAREN type_name RPAREN

type_qualifier::=
	  CONST
	| RESTRICT
	| VOLATILE
	| ATOMIC

attribute_type_qualifier::=
	  type_qualifier
	| type_qualifier attribute_specifier_sequence

function_specifier::=
	  INLINE
	| NORETURN

alignment_specifier::=
	  ALIGNAS LPAREN type_name RPAREN
	| ALIGNAS LPAREN constant_expression RPAREN

attribute_alignment_specifier::=
	  alignment_specifier
	| alignment_specifier attribute_specifier_sequence

declarator::=
	  direct_declarator
	| pointer direct_declarator

direct_declarator::=
	  general_identifier
	| general_identifier attribute_specifier_sequence
	| LPAREN save_context declarator RPAREN
	| array_declarator
	| array_declarator attribute_specifier_sequence
	| function_declarator
	| function_declarator attribute_specifier_sequence
	| direct_declarator LPAREN save_context RPAREN
	| direct_declarator LPAREN save_context identifier_list RPAREN

array_declarator::=
	  direct_declarator LBRACK option_type_qualifier_list_ option_assignment_expression_ RBRACK
	| direct_declarator LBRACK STATIC option_type_qualifier_list_ assignment_expression RBRACK
	| direct_declarator LBRACK type_qualifier_list STATIC assignment_expression RBRACK
	| direct_declarator LBRACK option_type_qualifier_list_ STAR RBRACK

function_declarator::=
	  direct_declarator LPAREN scoped_parameter_type_list_ RPAREN

identifier_list::=
	  var_name
	| identifier_list COMMA var_name

pointer::=
	  STAR option_type_qualifier_list_ option_pointer_
	| STAR attribute_specifier_sequence option_type_qualifier_list_ option_pointer_

type_qualifier_list::=
	  type_qualifier
	| type_qualifier_list type_qualifier

parameter_type_list::=
	  parameter_list save_context
	| parameter_list COMMA ELLIPSIS save_context

parameter_list::=
	  parameter_declaration
	| parameter_list COMMA parameter_declaration

parameter_declaration::=
	  declaration_specifiers declarator_varname
	| attribute_specifier_sequence declaration_specifiers declarator_varname
	| declaration_specifiers
	| declaration_specifiers abstract_declarator
	| attribute_specifier_sequence declaration_specifiers
	| attribute_specifier_sequence declaration_specifiers abstract_declarator

type_name::=
	  specifier_qualifier_list option_abstract_declarator_

abstract_declarator::=
	  pointer
	| direct_abstract_declarator
	| pointer direct_abstract_declarator

direct_abstract_declarator::=
	  LPAREN save_context abstract_declarator RPAREN
	| array_abstract_declarator
	| array_abstract_declarator attribute_specifier_sequence
	| function_abstract_declarator
	| function_abstract_declarator attribute_specifier_sequence

array_abstract_declarator::=
	  LBRACK option_assignment_expression_ RBRACK
	| LBRACK type_qualifier_list option_assignment_expression_ RBRACK
	| direct_abstract_declarator LBRACK option_assignment_expression_ RBRACK
	| direct_abstract_declarator LBRACK type_qualifier_list option_assignment_expression_ RBRACK
	| LBRACK STATIC option_type_qualifier_list_ assignment_expression RBRACK
	| direct_abstract_declarator LBRACK STATIC option_type_qualifier_list_ assignment_expression RBRACK
	| LBRACK type_qualifier_list STATIC assignment_expression RBRACK
	| direct_abstract_declarator LBRACK type_qualifier_list STATIC assignment_expression RBRACK
	| LBRACK STAR RBRACK
	| direct_abstract_declarator LBRACK STAR RBRACK

function_abstract_declarator::=
	  LPAREN option_scoped_parameter_type_list__ RPAREN
	| direct_abstract_declarator LPAREN option_scoped_parameter_type_list__ RPAREN

initializer_::=
	  assignment_expression
	| LBRACE initializer_list RBRACE
	| LBRACE initializer_list COMMA RBRACE

initializer_list::=
	  option_designation_ initializer_
	| initializer_list COMMA option_designation_ initializer_

designation::=
	  designator_list EQ

designator_list::=
	  designator
	| designator_list designator

designator::=
	  LBRACK constant_expression RBRACK
	| DOT general_identifier

static_assert_declaration::=
	  STATIC_ASSERT LPAREN constant_expression COMMA string_literal RPAREN SEMICOLON

statement::=
	  labeled_statement
	| option_attribute_specifier_sequence_ scoped_compound_statement_
	| expression_statement
	| option_attribute_specifier_sequence_ scoped_selection_statement_
	| option_attribute_specifier_sequence_ scoped_iteration_statement_
	| option_attribute_specifier_sequence_ jump_statement
	| asm_statement

labeled_statement::=
	  general_identifier COLON statement
	| attribute_specifier_sequence general_identifier COLON statement
	| option_attribute_specifier_sequence_ CASE constant_expression ELLIPSIS constant_expression COLON statement
	| option_attribute_specifier_sequence_ CASE constant_expression COLON statement
	| option_attribute_specifier_sequence_ DEFAULT COLON statement

compound_statement::=
	  LBRACE option_block_item_list_ RBRACE
	| LBRACES separated_nonempty_list_PIPES_statement_ RBRACES

block_item_list::=
	  block_item
	| block_item_list block_item

block_item::=
	  declaration
	| statement
	| CERB_MAGIC

expression_statement::=
	  option_expression_ SEMICOLON
	| attribute_specifier_sequence expression SEMICOLON

selection_statement::=
	  IF LPAREN expression RPAREN scoped_statement_
	| IF LPAREN expression RPAREN scoped_statement_ ELSE scoped_statement_
	| SWITCH LPAREN expression RPAREN scoped_statement_

magic_comment_list::=
	  magic_comment_list CERB_MAGIC
	| /*%empty*/

iteration_statement::=
	  WHILE LPAREN expression RPAREN magic_comment_list scoped_statement_
	| DO magic_comment_list scoped_statement_ WHILE LPAREN expression RPAREN SEMICOLON
	| FOR LPAREN option_expression_ SEMICOLON option_expression_ SEMICOLON option_expression_ RPAREN magic_comment_list scoped_statement_
	| FOR LPAREN declaration option_expression_ SEMICOLON option_expression_ RPAREN magic_comment_list scoped_statement_

jump_statement::=
	  GOTO general_identifier SEMICOLON
	| CONTINUE SEMICOLON
	| BREAK SEMICOLON
	| RETURN option_expression_ SEMICOLON

asm_register::=
	  ASM LPAREN string_literal RPAREN

asm_qualifier::=
	  VOLATILE
	| ASM_VOLATILE
	| INLINE
	| GOTO

asm_output_input::=
	  string_literal LPAREN expression RPAREN
	| LBRACK UNAME VARIABLE RBRACK string_literal LPAREN expression RPAREN
	| LBRACK LNAME VARIABLE RBRACK string_literal LPAREN expression RPAREN

asm_clobber::=
	  string_literal

asm_label::=
	  UNAME VARIABLE
	| LNAME VARIABLE

asm_with_output::=
	  COLON loption_separated_nonempty_list_COMMA_asm_output_input__ option_asm_with_input_

asm_with_input::=
	  COLON loption_separated_nonempty_list_COMMA_asm_output_input__ option_asm_with_clobbers_

asm_with_clobbers::=
	  COLON loption_separated_nonempty_list_COMMA_asm_clobber__ option_asm_with_labels_

asm_with_labels::=
	  COLON list_asm_label_

asm_statement::=
	  ASM list_asm_qualifier_ LPAREN string_literal RPAREN
	| ASM list_asm_qualifier_ LPAREN string_literal asm_with_output RPAREN

external_declaration_list::=
	  external_declaration
	| external_declaration_list external_declaration

external_declaration::=
	  CERB_MAGIC
	| function_definition
	| declaration

function_definition1::=
	  declaration_specifiers declarator_varname
	| attribute_specifier_sequence declaration_specifiers declarator_varname

function_definition::=
	  function_definition1 option_declaration_list_ magic_comment_list compound_statement boption_SEMICOLON_

declaration_list::=
	  no_leading_attribute_declaration
	| declaration_list no_leading_attribute_declaration

attribute_declaration::=
	  attribute_specifier_sequence SEMICOLON

attribute_specifier_sequence::=
	  attribute_specifier
	| attribute_specifier_sequence attribute_specifier

attribute_specifier::=
	  LBRACK_LBRACK attribute_list RBRACK RBRACK

attribute_list::=
	  attribute
	| attribute_list COMMA attribute

attribute::=
	  attribute_token option_attribute_argument_clause_

c_keyword_as_string::=
	  AUTO
	| BREAK
	| CASE
	| CHAR
	| CONST
	| CONTINUE
	| DEFAULT
	| DO
	| DOUBLE
	| ELSE
	| ENUM
	| EXTERN
	| FLOAT
	| FOR
	| GOTO
	| IF
	| INLINE
	| INT
	| LONG
	| REGISTER
	| RESTRICT
	| RETURN
	| SHORT
	| SIGNED
	| SIZEOF
	| STATIC
	| STRUCT
	| SWITCH
	| TYPEDEF
	| UNION
	| UNSIGNED
	| VOID
	| VOLATILE
	| WHILE
	| ALIGNAS
	| ALIGNOF
	| ATOMIC
	| BOOL
	| COMPLEX
	| GENERIC
	| NORETURN
	| STATIC_ASSERT
	| THREAD_LOCAL

attribute_identifier::=
	  general_identifier
	| c_keyword_as_string

attribute_token::=
	  attribute_identifier
	| attribute_prefixed_token

attribute_prefixed_token::=
	  attribute_identifier COLON_COLON attribute_identifier

attribute_argument_clause::=
	  LPAREN balanced_token_sequence RPAREN

balanced_token_sequence::=
	  balanced_token
	| balanced_token_sequence balanced_token

string_literal_component::=
	  STRING_LITERAL

string_literal::=
	  nonempty_list_string_literal_component_

located_string_literal::=
	  string_literal

balanced_token::=
	  LPAREN balanced_token_sequence RPAREN
	| LBRACK balanced_token_sequence RBRACK
	| LBRACE balanced_token_sequence RBRACE
	| separated_nonempty_list_COMMA_located_string_literal_

prim_expr::=
	  CN_NULL
	| CN_TRUE
	| CN_FALSE
	| CONSTANT
	| CN_CONSTANT
	| UNAME VARIABLE
	| LNAME VARIABLE
	| UNAME TYPE
	| LNAME TYPE
	| RETURN
	| prim_expr DOT UNAME VARIABLE
	| prim_expr DOT LNAME VARIABLE
	| prim_expr DOT UNAME TYPE
	| prim_expr DOT LNAME TYPE
	| prim_expr MINUS_GT UNAME VARIABLE
	| prim_expr MINUS_GT LNAME VARIABLE
	| prim_expr MINUS_GT UNAME TYPE
	| prim_expr MINUS_GT LNAME TYPE
	| LPAREN expr RPAREN
	| CN_ARRAY_SHIFT LT ctype GT LPAREN expr COMMA expr RPAREN
	| CN_ARRAY_SHIFT LPAREN expr COMMA expr RPAREN
	| CN_MEMBER_SHIFT LPAREN expr COMMA UNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LPAREN expr COMMA LNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LPAREN expr COMMA UNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LPAREN expr COMMA LNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT UNAME VARIABLE GT LPAREN expr COMMA UNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT UNAME VARIABLE GT LPAREN expr COMMA LNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT UNAME VARIABLE GT LPAREN expr COMMA UNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT UNAME VARIABLE GT LPAREN expr COMMA LNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT LNAME VARIABLE GT LPAREN expr COMMA UNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT LNAME VARIABLE GT LPAREN expr COMMA LNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT LNAME VARIABLE GT LPAREN expr COMMA UNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT LNAME VARIABLE GT LPAREN expr COMMA LNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT UNAME TYPE GT LPAREN expr COMMA UNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT UNAME TYPE GT LPAREN expr COMMA LNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT UNAME TYPE GT LPAREN expr COMMA UNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT UNAME TYPE GT LPAREN expr COMMA LNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT LNAME TYPE GT LPAREN expr COMMA UNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT LNAME TYPE GT LPAREN expr COMMA LNAME VARIABLE RPAREN
	| CN_MEMBER_SHIFT LT LNAME TYPE GT LPAREN expr COMMA UNAME TYPE RPAREN
	| CN_MEMBER_SHIFT LT LNAME TYPE GT LPAREN expr COMMA LNAME TYPE RPAREN
	| UNAME VARIABLE LPAREN loption_separated_nonempty_list_COMMA_expr__ RPAREN
	| LNAME VARIABLE LPAREN loption_separated_nonempty_list_COMMA_expr__ RPAREN
	| UNAME TYPE LPAREN loption_separated_nonempty_list_COMMA_expr__ RPAREN
	| LNAME TYPE LPAREN loption_separated_nonempty_list_COMMA_expr__ RPAREN
	| cn_good LPAREN expr RPAREN
	| UNAME VARIABLE cons_args
	| LNAME VARIABLE cons_args
	| UNAME TYPE cons_args
	| LNAME TYPE cons_args
	| prim_expr LBRACK expr RBRACK
	| LBRACE expr RBRACE PERCENT UNAME VARIABLE
	| LBRACE expr RBRACE PERCENT LNAME VARIABLE
	| STRUCT UNAME VARIABLE LBRACE record_def RBRACE
	| STRUCT LNAME VARIABLE LBRACE record_def RBRACE
	| STRUCT UNAME TYPE LBRACE record_def RBRACE
	| STRUCT LNAME TYPE LBRACE record_def RBRACE
	| LBRACE record_def RBRACE
	| LBRACE nonempty_member_updates RBRACE
	| prim_expr LBRACK separated_nonempty_list_COMMA_index_update_ RBRACK
	| DEFAULT LT base_type GT

unary_expr::=
	  prim_expr
	| STAR unary_expr
	| SIZEOF LT ctype GT
	| OFFSETOF LPAREN UNAME VARIABLE COMMA UNAME VARIABLE RPAREN
	| OFFSETOF LPAREN UNAME VARIABLE COMMA LNAME VARIABLE RPAREN
	| OFFSETOF LPAREN UNAME VARIABLE COMMA UNAME TYPE RPAREN
	| OFFSETOF LPAREN UNAME VARIABLE COMMA LNAME TYPE RPAREN
	| OFFSETOF LPAREN LNAME VARIABLE COMMA UNAME VARIABLE RPAREN
	| OFFSETOF LPAREN LNAME VARIABLE COMMA LNAME VARIABLE RPAREN
	| OFFSETOF LPAREN LNAME VARIABLE COMMA UNAME TYPE RPAREN
	| OFFSETOF LPAREN LNAME VARIABLE COMMA LNAME TYPE RPAREN
	| OFFSETOF LPAREN UNAME TYPE COMMA UNAME VARIABLE RPAREN
	| OFFSETOF LPAREN UNAME TYPE COMMA LNAME VARIABLE RPAREN
	| OFFSETOF LPAREN UNAME TYPE COMMA UNAME TYPE RPAREN
	| OFFSETOF LPAREN UNAME TYPE COMMA LNAME TYPE RPAREN
	| OFFSETOF LPAREN LNAME TYPE COMMA UNAME VARIABLE RPAREN
	| OFFSETOF LPAREN LNAME TYPE COMMA LNAME VARIABLE RPAREN
	| OFFSETOF LPAREN LNAME TYPE COMMA UNAME TYPE RPAREN
	| OFFSETOF LPAREN LNAME TYPE COMMA LNAME TYPE RPAREN
	| LBRACE expr RBRACE CN_UNCHANGED
	| MINUS unary_expr
	| BANG unary_expr
	| TILDE unary_expr
	| AMPERSAND LPAREN prim_expr MINUS_GT UNAME VARIABLE RPAREN
	| AMPERSAND LPAREN prim_expr MINUS_GT LNAME VARIABLE RPAREN
	| AMPERSAND LPAREN prim_expr MINUS_GT UNAME TYPE RPAREN
	| AMPERSAND LPAREN prim_expr MINUS_GT LNAME TYPE RPAREN
	| AMPERSAND UNAME VARIABLE
	| AMPERSAND LNAME VARIABLE
	| AMPERSAND UNAME TYPE
	| AMPERSAND LNAME TYPE
	| LPAREN base_type_explicit RPAREN unary_expr

mul_expr::=
	  unary_expr
	| mul_expr AMPERSAND unary_expr
	| mul_expr CARET unary_expr
	| mul_expr STAR unary_expr
	| mul_expr SLASH unary_expr
	| mul_expr PERCENT unary_expr

add_expr::=
	  mul_expr
	| add_expr PLUS mul_expr
	| add_expr MINUS mul_expr
	| add_expr PIPE mul_expr

rel_expr::=
	  add_expr
	| rel_expr EQ_EQ add_expr
	| rel_expr BANG_EQ add_expr
	| rel_expr LT add_expr
	| rel_expr GT add_expr
	| rel_expr LT_EQ add_expr
	| rel_expr GT_EQ add_expr

bool_and_expr::=
	  rel_expr
	| bool_and_expr AMPERSAND_AMPERSAND rel_expr

bool_implies_expr::=
	  bool_and_expr
	| bool_and_expr CN_IMPLIES bool_implies_expr

bool_or_expr::=
	  bool_implies_expr
	| bool_or_expr PIPE_PIPE bool_implies_expr

list_expr::=
	  bool_or_expr
	| LBRACK separated_nonempty_list_COMMA_rel_expr_ RBRACK

int_range::=
	  CONSTANT COMMA CONSTANT

member_def::=
	  UNAME VARIABLE COLON expr
	| LNAME VARIABLE COLON expr
	| UNAME TYPE COLON expr
	| LNAME TYPE COLON expr

member_updates::=
	  member_def COMMA member_updates
	| DOT DOT expr

nonempty_member_updates::=
	  member_def COMMA member_updates

index_update::=
	  prim_expr COLON expr

match_cases::=
	  match_case
	| match_cases match_case

pattern_member_def::=
	  UNAME VARIABLE COLON pattern
	| LNAME VARIABLE COLON pattern
	| UNAME TYPE COLON pattern
	| LNAME TYPE COLON pattern

pattern_cons_args::=
	  LBRACE loption_separated_nonempty_list_COMMA_pattern_member_def__ RBRACE

pattern::=
	  CN_WILD
	| UNAME VARIABLE
	| LNAME VARIABLE
	| UNAME TYPE
	| LNAME TYPE
	| UNAME VARIABLE pattern_cons_args
	| LNAME VARIABLE pattern_cons_args
	| UNAME TYPE pattern_cons_args
	| LNAME TYPE pattern_cons_args

match_case::=
	  pattern EQ GT LBRACE expr RBRACE

match_target::=
	  UNAME VARIABLE
	| LNAME VARIABLE
	| UNAME TYPE
	| LNAME TYPE
	| LPAREN expr RPAREN

expr_without_let::=
	  list_expr
	| list_expr QUESTION list_expr COLON list_expr
	| IF LPAREN expr RPAREN LBRACE expr RBRACE ELSE LBRACE expr RBRACE
	| CN_EACH LPAREN base_type UNAME VARIABLE COLON int_range SEMICOLON expr RPAREN
	| CN_EACH LPAREN base_type LNAME VARIABLE COLON int_range SEMICOLON expr RPAREN
	| CN_EACH LPAREN base_type UNAME TYPE COLON int_range SEMICOLON expr RPAREN
	| CN_EACH LPAREN base_type LNAME TYPE COLON int_range SEMICOLON expr RPAREN
	| CN_MATCH match_target LBRACE match_cases RBRACE

expr::=
	  expr_without_let
	| CN_LET UNAME VARIABLE EQ expr SEMICOLON expr
	| CN_LET LNAME VARIABLE EQ expr SEMICOLON expr
	| CN_LET UNAME TYPE EQ expr SEMICOLON expr
	| CN_LET LNAME TYPE EQ expr SEMICOLON expr

base_type_explicit::=
	  VOID
	| CN_BOOL
	| CN_INTEGER
	| CN_BITS
	| CN_REAL
	| CN_POINTER
	| CN_ALLOC_ID
	| LBRACE nonempty_cn_params RBRACE
	| STRUCT UNAME VARIABLE
	| STRUCT LNAME VARIABLE
	| STRUCT UNAME TYPE
	| STRUCT LNAME TYPE
	| CN_DATATYPE UNAME VARIABLE
	| CN_DATATYPE LNAME VARIABLE
	| CN_DATATYPE UNAME TYPE
	| CN_DATATYPE LNAME TYPE
	| CN_MAP LT base_type COMMA base_type GT
	| CN_LIST LT base_type GT
	| CN_TUPLE LT loption_separated_nonempty_list_COMMA_base_type__ GT
	| CN_SET LT base_type GT

base_type::=
	  base_type_explicit
	| UNAME VARIABLE
	| LNAME VARIABLE
	| UNAME TYPE
	| LNAME TYPE

cn_good::=
	  CN_GOOD LT ctype GT

nonempty_cn_params::=
	  separated_nonempty_list_COMMA_base_type_cn_variable_

record_def::=
	  separated_nonempty_list_COMMA_member_def_

cons_args::=
	  LBRACE loption_separated_nonempty_list_COMMA_member_def__ RBRACE

ctype::=
	  type_name

option_COMMA_::=
	  /*%empty*/
	| COMMA

option_abstract_declarator_::=
	  /*%empty*/
	| abstract_declarator

option_argument_expression_list_::=
	  /*%empty*/
	| argument_expression_list

option_asm_with_clobbers_::=
	  /*%empty*/
	| asm_with_clobbers

option_asm_with_input_::=
	  /*%empty*/
	| asm_with_input

option_asm_with_labels_::=
	  /*%empty*/
	| asm_with_labels

option_assignment_expression_::=
	  /*%empty*/
	| assignment_expression

option_attribute_argument_clause_::=
	  /*%empty*/
	| attribute_argument_clause

option_attribute_specifier_sequence_::=
	  /*%empty*/
	| attribute_specifier_sequence

option_block_item_list_::=
	  /*%empty*/
	| block_item_list

option_declaration_list_::=
	  /*%empty*/
	| declaration_list

option_declarator_::=
	  /*%empty*/
	| declarator

option_designation_::=
	  /*%empty*/
	| designation

option_expression_::=
	  /*%empty*/
	| expression

option_general_identifier_::=
	  /*%empty*/
	| general_identifier

option_init_declarator_list_declarator_typedefname__::=
	  /*%empty*/
	| init_declarator_list_declarator_typedefname_

option_init_declarator_list_declarator_varname__::=
	  /*%empty*/
	| init_declarator_list_declarator_varname_

option_pointer_::=
	  /*%empty*/
	| pointer

option_scoped_parameter_type_list__::=
	  /*%empty*/
	| scoped_parameter_type_list_

option_struct_declarator_list_::=
	  /*%empty*/
	| struct_declarator_list

option_type_qualifier_list_::=
	  /*%empty*/
	| type_qualifier_list

boption_SEMICOLON_::=
	  /*%empty*/
	| SEMICOLON

boption_nonempty_list_SEMICOLON__::=
	  /*%empty*/
	| nonempty_list_SEMICOLON_

loption_separated_nonempty_list_COMMA_asm_clobber__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_asm_clobber_

loption_separated_nonempty_list_COMMA_asm_output_input__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_asm_output_input_

loption_separated_nonempty_list_COMMA_base_type__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_base_type_

loption_separated_nonempty_list_COMMA_expr__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_expr_

loption_separated_nonempty_list_COMMA_member_def__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_member_def_

loption_separated_nonempty_list_COMMA_pattern_member_def__::=
	  /*%empty*/
	| separated_nonempty_list_COMMA_pattern_member_def_

list_asm_label_::=
	  /*%empty*/
	| asm_label list_asm_label_

list_asm_qualifier_::=
	  /*%empty*/
	| asm_qualifier list_asm_qualifier_

list_declaration_specifier_::=
	  /*%empty*/
	| declaration_specifier list_declaration_specifier_

nonempty_list_SEMICOLON_::=
	  SEMICOLON
	| SEMICOLON nonempty_list_SEMICOLON_

nonempty_list_string_literal_component_::=
	  string_literal_component
	| string_literal_component nonempty_list_string_literal_component_

separated_nonempty_list_COMMA_asm_clobber_::=
	  asm_clobber
	| asm_clobber COMMA separated_nonempty_list_COMMA_asm_clobber_

separated_nonempty_list_COMMA_asm_output_input_::=
	  asm_output_input
	| asm_output_input COMMA separated_nonempty_list_COMMA_asm_output_input_

separated_nonempty_list_COMMA_base_type_::=
	  base_type
	| base_type COMMA separated_nonempty_list_COMMA_base_type_

separated_nonempty_list_COMMA_base_type_cn_variable_::=
	  base_type UNAME VARIABLE
	| base_type LNAME VARIABLE
	| base_type UNAME TYPE
	| base_type LNAME TYPE
	| base_type UNAME VARIABLE COMMA separated_nonempty_list_COMMA_base_type_cn_variable_
	| base_type LNAME VARIABLE COMMA separated_nonempty_list_COMMA_base_type_cn_variable_
	| base_type UNAME TYPE COMMA separated_nonempty_list_COMMA_base_type_cn_variable_
	| base_type LNAME TYPE COMMA separated_nonempty_list_COMMA_base_type_cn_variable_

separated_nonempty_list_COMMA_expr_::=
	  expr
	| expr COMMA separated_nonempty_list_COMMA_expr_

separated_nonempty_list_COMMA_index_update_::=
	  index_update
	| index_update COMMA separated_nonempty_list_COMMA_index_update_

separated_nonempty_list_COMMA_located_string_literal_::=
	  located_string_literal
	| located_string_literal COMMA separated_nonempty_list_COMMA_located_string_literal_

separated_nonempty_list_COMMA_member_def_::=
	  member_def
	| member_def COMMA separated_nonempty_list_COMMA_member_def_

separated_nonempty_list_COMMA_pattern_member_def_::=
	  pattern_member_def
	| pattern_member_def COMMA separated_nonempty_list_COMMA_pattern_member_def_

separated_nonempty_list_COMMA_rel_expr_::=
	  rel_expr
	| rel_expr COMMA separated_nonempty_list_COMMA_rel_expr_

separated_nonempty_list_PIPES_statement_::=
	  statement
	| statement PIPES separated_nonempty_list_PIPES_statement_

//Tokens

AUTO ::= "auto"
BREAK ::= "break"
CASE ::= "case"
CHAR ::= "char"
CONST ::= "const"
CONTINUE ::= "continue"
DEFAULT ::= "default"
DO ::= "do"
DOUBLE ::= "double"
ELSE ::= "else"
ENUM ::= "enum"
EXTERN ::= "extern"
FLOAT ::= "float"
FOR ::= "for"
GOTO ::= "goto"
IF ::= "if"
INLINE ::= "inline"
INT ::= "int"
LONG ::= "long"
REGISTER ::= "register"
RESTRICT ::= "restrict"
RETURN ::= "return"
SHORT ::= "short"
SIGNED ::= "signed"
SIZEOF ::= "sizeof"
STATIC ::= "static"
STRUCT ::= "struct"
SWITCH ::= "switch"
TYPEDEF ::= "typedef"
TYPEOF ::= "typeof"
UNION ::= "union"
UNSIGNED ::= "unsigned"
VOID ::= "void"
VOLATILE ::= "volatile"
WHILE ::= "while"
ALIGNAS ::= "_Alignas"
ALIGNOF ::= "_Alignof"
ATOMIC ::= "_Atomic"
BOOL ::= "_Bool"
COMPLEX ::= "_Complex"
GENERIC ::= "_Generic"
/* IMAGINARY ::= "_Imaginary"      */
NORETURN ::= "_Noreturn"
STATIC_ASSERT ::= "_Static_assert"
THREAD_LOCAL ::= "_Thread_local"

ASSERT ::= "assert"
OFFSETOF ::= "offsetof"
VA_START ::= "__cerb_va_start"
VA_COPY ::= "__cerb_va_copy"
VA_ARG ::= "__cerb_va_arg"
VA_END ::= "__cerb_va_end"

PRINT_TYPE ::= "__cerb_printtype"

BMC_ASSUME ::= "__BMC_ASSUME"

/* some GCC extensions */
ASM ::= "asm"
ASM ::= "__asm__"
ASM_VOLATILE ::= "__volatile__"
BUILTIN_TYPES_COMPATIBLE_P ::= "__builtin_types_compatible_p"
BUILTIN_CHOOSE_EXPR ::= "__builtin_choose_expr"


/* CN 'production' keywords: well-supported and suitable for general use */
CN_GOOD ::= "good"
CN_BOOL ::= "boolean"
CN_INTEGER ::= "integer"
CN_BITS ::= "u8"
CN_BITS ::= "u16" 
CN_BITS ::= "u32"
CN_BITS ::= "u64"
CN_BITS ::= "u128"
CN_BITS ::= "i8"
CN_BITS ::= "i16"
CN_BITS ::= "i32"
CN_BITS ::= "i64"
CN_BITS ::= "i128"
CN_REAL ::= "real"
CN_POINTER ::= "pointer"
CN_ALLOC_ID ::= "alloc_id"
CN_MAP ::= "map"
CN_LET ::= "let"
CN_TAKE ::= "take"
CN_OWNED ::= "Owned"
CN_BLOCK ::= "Block"
CN_EACH ::= "each"
CN_NULL ::= "NULL"
CN_TRUE ::= "true"
CN_FALSE ::= "false"
CN_REQUIRES ::= "requires"
CN_ENSURES ::= "ensures"
CN_INV ::= "inv"
CN_ACCESSES ::= "accesses"
CN_TRUSTED ::= "trusted"
CN_SPEC ::= "spec"
CN_UNCHANGED ::= "unchanged"
CN_INSTANTIATE ::= "instantiate"
CN_SPLIT_CASE ::= "split_case"
CN_EXTRACT ::= "extract"
CN_ARRAY_SHIFT ::= "array_shift"
CN_MEMBER_SHIFT ::= "member_shift"
CN_UNFOLD ::= "unfold"
CN_APPLY ::= "apply"
CN_MATCH ::= "match"
CN_PREDICATE ::= "predicate"
CN_FUNCTION ::= "function"
CN_LEMMA ::= "lemma"
CN_DATATYPE ::= "datatype"
CN_TYPE_SYNONYM ::= "type_synonym"
CN_WILD ::= "_"
CN_IMPLIES ::= "implies"

/* CN 'experimental' keywords - functional in some cases but not recommended for
general use */
CN_LIST ::= "cn_list"
CN_TUPLE ::= "cn_tuple"
CN_SET ::= "cn_set"
CN_HAVE ::= "cn_have"
CN_FUNCTION ::= "cn_function"
CN_PRINT ::= "cn_print"
CN_TO_BYTES ::= "to_bytes"
CN_FROM_BYTES ::= "from_bytes"

/* CN 'unimplemented' keywords - non-functionalbut the keyword is reserved */
CN_PACK ::= "pack"
CN_UNPACK ::= "unpack"

/* STD §6.4.6#1 Punctuators */
LBRACK ::= '['              
RBRACK ::= ']'              
LPAREN ::= '('              
RPAREN ::= ')'              
LBRACE ::= '{'              
RBRACE ::= '}'              
DOT ::= '.'  
MINUS_GT ::= "->"            
PLUS_PLUS ::= "++"           
MINUS_MINUS ::= "--"         
AMPERSAND ::= '&'           
STAR ::= '*' 
PLUS ::= '+' 
MINUS ::= '-'
TILDE ::= '~'
BANG ::= '!' 
SLASH ::= '/'
PERCENT ::= '%'             
LT_LT ::= "<<"
GT_GT ::= ">>"
LT ::= '<'   
GT ::= '>'   
LT_EQ ::= "<="
GT_EQ ::= ">="
EQ_EQ ::= "=="
BANG_EQ ::= "!="             
CARET ::= '^'
PIPE ::= '|' 
AMPERSAND_AMPERSAND ::= "&&" 
PIPE_PIPE ::= "||"           
QUESTION ::= '?'            
COLON_COLON ::= "::"         
COLON ::= ':'
SEMICOLON ::= ';'           
ELLIPSIS ::= "..."            
EQ ::= '='   
STAR_EQ ::= "*="             
SLASH_EQ ::= "/="            
PERCENT_EQ ::= "%="          
PLUS_EQ ::= "+="             
MINUS_EQ ::= "-="            
LT_LT_EQ ::= "<<="            
GT_GT_EQ ::= ">>="            
AMPERSAND_EQ ::= "&="        
CARET_EQ ::= "^="            
PIPE_EQ ::= "|="             
COMMA ::= ','
LBRACK_LBRACK ::= "{{" 
/*  | rbrack_rbrack RBRACK_RBRACK } */
/*  | '#'  */
/*  | "##" */

/* STD §6.4.6#3 */
LBRACK ::= "<:" 
RBRACK ::= ":>" 
LBRACE ::= "<%" 
RBRACE ::= "%>" 
/*  | "%:"   */
/*  | "%:%:" */

/* NON-STD GNU extensions */
QUESTION_COLON ::= "?:" 

/* NON-STD (cppmem-like thread syntax) */
LBRACES ::= "{-{" 
PIPES ::= "|||"   
RBRACES ::= "}-}"

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Grammar railroad diagram #897

Grammar railroad diagram #897

mingodad commented Mar 2, 2025

mingodad commented Mar 2, 2025

Grammar railroad diagram #897

Grammar railroad diagram #897

Comments

mingodad commented Mar 2, 2025

mingodad commented Mar 2, 2025