From 5f1eaa828ccb3dbcd11980b113267f685c39ced2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 13 Jan 2021 16:26:16 +0100
Subject: [PATCH] [logic] Allows any integral constant in an array size, not
just decimal ones.
---
src/kernel_internals/parsing/logic_lexer.mll | 16 ++++++------
src/kernel_internals/parsing/logic_parser.mly | 22 ++++++++++------
tests/spec/oracle/qarrsize.res.oracle | 16 ++++++++++++
tests/spec/qarrsize.c | 25 +++++++++++++++++++
4 files changed, 63 insertions(+), 16 deletions(-)
create mode 100644 tests/spec/oracle/qarrsize.res.oracle
create mode 100644 tests/spec/qarrsize.c
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index d31c8c679e0..c16497fde98 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -367,17 +367,17 @@ rule token = parse
end else curr_tok
}
- | '0'['x''X'] rH+ rIS? { CONSTANT (IntConstant (lexeme lexbuf)) }
- | '0'['b''B'] rB+ rIS? { CONSTANT (IntConstant (lexeme lexbuf)) }
- | '0' rD+ rIS? { CONSTANT (IntConstant (lexeme lexbuf)) }
- | rD+ { CONSTANT10 (lexeme lexbuf) }
- | rD+ rIS { CONSTANT (IntConstant (lexeme lexbuf)) }
+ | '0'['x''X'] rH+ rIS? { INT_CONSTANT (lexeme lexbuf) }
+ | '0'['b''B'] rB+ rIS? { INT_CONSTANT (lexeme lexbuf) }
+ | '0' rD+ rIS? { INT_CONSTANT (lexeme lexbuf) }
+ | rD+ { INT_CONSTANT (lexeme lexbuf) }
+ | rD+ rIS { INT_CONSTANT (lexeme lexbuf) }
| ('L'? "'" as prelude) (([^ '\\' '\'' '\n']|("\\"[^ '\n']))+ as content) "'"
{
let b = Buffer.create 5 in
Buffer.add_string b prelude;
let lbf = Lexing.from_string content in
- CONSTANT (IntConstant (chr b lbf ^ "'"))
+ INT_CONSTANT (chr b lbf ^ "'")
}
(* floating-point literals, both decimal and hexadecimal *)
| rD+ rE rFS?
@@ -386,11 +386,11 @@ rule token = parse
| '0'['x''X'] rH+ '.' rH* rP rFS?
| '0'['x''X'] rH* '.' rH+ rP rFS?
| '0'['x''X'] rH+ rP rFS?
- { CONSTANT (FloatConstant (lexeme lexbuf)) }
+ { FLOAT_CONSTANT (lexeme lexbuf) }
(* hack to lex 0..3 as 0 .. 3 and not as 0. .3 *)
| (rD+ as n) ".." { lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos - 2;
- CONSTANT (IntConstant n) }
+ INT_CONSTANT n }
| 'L'? '"' as prelude (([^ '\\' '"' '\n']|("\\"[^ '\n']))* as content) '"'
{ STRING_LITERAL (prelude.[0] = 'L',content) }
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 8a41fe69f4f..ab09ffd36dc 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -264,8 +264,10 @@
/* ACSL extension for external spec file */
%token <string> IDENTIFIER TYPENAME
%token <bool*string> STRING_LITERAL
-%token <Logic_ptree.constant> CONSTANT
-%token <string> CONSTANT10
+%token <string> INT_CONSTANT
+%token <string> FLOAT_CONSTANT
+%token <string> STRING_CONSTANT
+%token <string> WSTRING_CONSTANT
%token LPAR RPAR IF ELSE COLON COLON2 COLONCOLON DOT DOTDOT DOTDOTDOT
%token INT INTEGER REAL BOOLEAN BOOL FLOAT LT GT LE GE EQ NE COMMA ARROW EQUAL
%token FORALL EXISTS IFF IMPLIES AND OR NOT SEPARATED
@@ -678,12 +680,14 @@ var_spec:
;
constant:
-| CONSTANT { $1 }
-| CONSTANT10 { IntConstant $1 }
+| INT_CONSTANT { IntConstant $1 }
+| FLOAT_CONSTANT { FloatConstant $1 }
+| STRING_CONSTANT { StringConstant $1 }
+| WSTRING_CONSTANT { WStringConstant $1 }
;
array_size:
-| CONSTANT10 { ASinteger $1 }
+| INT_CONSTANT { ASinteger $1 }
| identifier { ASidentifier $1 }
| /* empty */ { ASnone }
;
@@ -1040,7 +1044,7 @@ ext_contract_markup:
stmt_markup:
| any_identifier { $1 }
-| CONSTANT10 { $1 }
+| INT_CONSTANT { $1 }
;
stmt_markup_attr:
@@ -2041,8 +2045,10 @@ wildcard:
| COLON2 { () }
| COLONCOLON { () }
| COMMA { () }
-| CONSTANT { () }
-| CONSTANT10 { () }
+| INT_CONSTANT { () }
+| FLOAT_CONSTANT { () }
+| STRING_CONSTANT { () }
+| WSTRING_CONSTANT { () }
| DOLLAR { () }
| DOT { () }
| DOTDOT { () }
diff --git a/tests/spec/oracle/qarrsize.res.oracle b/tests/spec/oracle/qarrsize.res.oracle
new file mode 100644
index 00000000000..d5b9c2f7b00
--- /dev/null
+++ b/tests/spec/oracle/qarrsize.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing tests/spec/qarrsize.c (with preprocessing)
+/* Generated by Frama-C */
+int a[0xFFu];
+int b[128L];
+int c[0x8A];
+int sa = (int)sizeof(int [0xFFu]);
+int sb = (int)sizeof(int [128L]);
+int sc = (int)sizeof(int [0x8A]);
+/*@ requires \valid(n + (0 .. sizeof(int [0xFFu])));
+ requires \valid(p + (0 .. sizeof(int [128L])));
+ requires \valid(q + (0 .. sizeof(int [0x8A])));
+ assigns \nothing;
+ */
+void f(int *n, int *p, int *q);
+
+
diff --git a/tests/spec/qarrsize.c b/tests/spec/qarrsize.c
new file mode 100644
index 00000000000..50c0f886d77
--- /dev/null
+++ b/tests/spec/qarrsize.c
@@ -0,0 +1,25 @@
+// Qualified Type-Array Size
+
+#define N 0xFFu
+#define P 128L
+#define Q 0x8A
+
+int a[N];
+int b[P];
+int c[Q];
+
+typedef int Ta[N];
+typedef int Tb[P];
+typedef int Tc[Q];
+
+int sa = sizeof(int[N]);
+int sb = sizeof(int[P]);
+int sc = sizeof(int[Q]);
+
+/*@
+ requires \valid(n + (0 .. sizeof(int[N])));
+ requires \valid(p + (0 .. sizeof(int[P])));
+ requires \valid(q + (0 .. sizeof(int[Q])));
+ assigns \nothing;
+ */
+void f(int *n, int *p, int *q);
--
GitLab