diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly index 4682d062852293c556e40b1caa5db36605c84fc2..3c14abf92a62cb1388f673783a14aa9470f3d836 100644 --- a/src/kernel_internals/parsing/logic_parser.mly +++ b/src/kernel_internals/parsing/logic_parser.mly @@ -1765,15 +1765,23 @@ any_identifier_non_logic: | identifier_or_typename { $1 } | non_logic_keyword { $1 } -identifier_or_typename: +identifier_or_typename: /* allowed as C field names */ +| TYPENAME { $1 } /* followed by the same list than 'identifier' */ | IDENTIFIER { $1 } -| TYPENAME { $1 } +/* token list used inside ascl clauses: */ +| BEHAVIORS { "behaviors" } +| LABEL { "label" } +| READS { "reads" } +| WRITES { "writes" } ; -identifier: +identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */ | IDENTIFIER { $1 } -| READS { "reads" } -| WRITES { "writes" } +/* token list used inside ascl clauses: */ +| BEHAVIORS { "behaviors" } +| LABEL { "label" } +| READS { "reads" } +| WRITES { "writes" } ; bounded_var: @@ -1786,30 +1794,30 @@ bounded_var: ; c_keyword: -| CASE { "case" } -| CHAR { "char" } -| BOOLEAN { "boolean" } -| BOOL { "_Bool" } -| CONST { "const" } -| DOUBLE { "double" } -| ELSE { "else" } -| ENUM { "enum" } -| FLOAT { "float" } -| IF { "if" } -| INT { "int" } -| LONG { "long" } -| SHORT { "short" } -| SIGNED { "signed" } -| SIZEOF { "sizeof" } -| STATIC { "static" } -| STRUCT { "struct" } -| UNION { "union" } +| CHAR { "char" } +| BOOLEAN { "boolean" } +| BOOL { "_Bool" } +| CONST { "const" } +| DOUBLE { "double" } +| ENUM { "enum" } +| ELSE { "else" } +| FLOAT { "float" } +| IF { "if" } +| INT { "int" } +| LONG { "long" } +| SHORT { "short" } +| SIGNED { "signed" } +| SIZEOF { "sizeof" } +| STATIC { "static" } +| STRUCT { "struct" } +| UNION { "union" } | UNSIGNED { "unsigned" } -| VOID { "void" } +| VOID { "void" } ; acsl_c_keyword: -| FOR { "for" } +| CASE { "case" } +| FOR { "for" } | VOLATILE { "volatile" } ; @@ -1848,7 +1856,7 @@ is_acsl_decl_or_code_annot: | LEMMA { "lemma" } | LOOP { "loop" } | PRAGMA { "pragma" } -| PREDICATE { "predicate" } +| PREDICATE { "predicate" } | SLICE { "slice" } | TYPE { "type" } | MODEL { "model" } @@ -1858,12 +1866,8 @@ is_acsl_decl_or_code_annot: ; is_acsl_other: -| BEHAVIORS { "behaviors" } -| INTEGER { "integer" } -| LABEL { "label" } -| READS { "reads" } -| REAL { "real" } -| WRITES { "writes" } +| INTEGER { "integer" (* token that cannot be used in C fields *) } +| REAL { "real" (* token that cannot be used in C fields *) } ; is_ext_spec: @@ -1876,7 +1880,7 @@ is_ext_spec: ; keyword: -| LOGIC { "logic" } +| LOGIC { "logic" } | non_logic_keyword { $1 } ; @@ -1887,7 +1891,7 @@ non_logic_keyword: | is_acsl_spec { $1 } | is_acsl_decl_or_code_annot { $1 } | is_acsl_other { $1 } -| CUSTOM { "custom" } +| CUSTOM { "custom" (* token that cannot be used in C fields *) } ; bs_keyword: diff --git a/tests/spec/kw.c b/tests/spec/kw.c index eb7b4e0b8fb456a73b66648f3d8fbd1b4cb9fd81..e57a4869f38f02d6bb9c79f6e7c7b1b7139b50fc 100644 --- a/tests/spec/kw.c +++ b/tests/spec/kw.c @@ -11,6 +11,12 @@ assert behavior = 0; int main () { //@ slevel 4; behavior++; + struct custom { int reads, behaviors, label ; } writes; + //@ assert custom: writes.reads + writes.behaviors <= \let global = writes.label; global; + struct at { int module, function, global ; } include; + //@ assert at: include.function + include.module <= \let behaviors = include.global ; behaviors; + struct loop { int requires, ensures, checks ; } assert; + //@ assert loop: assert.ensures + assert.ensures <= \let reads = assert.checks; reads ; return 0; } diff --git a/tests/spec/oracle/kw.res.oracle b/tests/spec/oracle/kw.res.oracle index b9d920cb849457f0161ca7ed3551f23b325e6cd8..151e9f04be62d2f30bcb233eb0ecfdff185f31d8 100644 --- a/tests/spec/oracle/kw.res.oracle +++ b/tests/spec/oracle/kw.res.oracle @@ -1,6 +1,21 @@ [kernel] Parsing tests/spec/kw.c (with preprocessing) /* Generated by Frama-C */ typedef int assert; +struct custom { + int reads ; + int behaviors ; + int label ; +}; +struct at { + int module ; + int function ; + int global ; +}; +struct loop { + int requires ; + int ensures ; + int checks ; +}; assert behavior = 0; /*@ logic assert foo(assert x) = x; */ @@ -12,8 +27,30 @@ assert behavior = 0; int main(void) { int __retres; + struct custom writes; + struct at include; + struct loop assert; /*@ slevel 4; */ behavior ++; + /*@ + assert + custom: + writes.reads + writes.behaviors ≤ (\let global = writes.label; global); + */ + ; + /*@ + assert + at: + include.function + include.module ≤ + (\let behaviors = include.global; behaviors); + */ + ; + /*@ + assert + loop: + assert.ensures + assert.ensures ≤ (\let reads = assert.checks; reads); + */ + ; __retres = 0; return __retres; }