From 238906ab7f71fafa11d637cc9d302c3398100d1a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 20 Oct 2021 08:39:40 +0200
Subject: [PATCH] [Cabs2cil] emit proper error message for unsupported
attribute vector_size
---
src/kernel_internals/typing/cabs2cil.ml | 9 +++++++--
tests/syntax/attributes-declarations-definitions.c | 10 ++++++++++
...> attributes-declarations-definitions.0.res.oracle} | 8 ++++----
.../attributes-declarations-definitions.1.res.oracle | 10 ++++++++++
4 files changed, 31 insertions(+), 6 deletions(-)
rename tests/syntax/oracle/{attributes-declarations-definitions.res.oracle => attributes-declarations-definitions.0.res.oracle} (90%)
create mode 100644 tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 264239138bb..3b2e601d3e9 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -84,7 +84,11 @@ end
let func_locs () = FuncLocs.get ()
-let stripUnderscore s =
+(* Attributes which are entirely unsupported by Frama-C and must cause a
+ parsing error, since their behavior requires non-standard parsing *)
+let unsupported_attributes = ["vector_size"]
+
+let stripUnderscore ?(checkUnsupported=true) s =
if String.length s = 1 then begin
if s = "_" then
Kernel.error ~once:true ~current:true "Invalid attribute name %s" s;
@@ -93,6 +97,8 @@ let stripUnderscore s =
let res = Extlib.strip_underscore s in
if res = "" then
Kernel.error ~once:true ~current:true "Invalid attribute name %s" s;
+ if checkUnsupported && List.mem res unsupported_attributes then
+ Kernel.error ~current:true "unsupported attribute: %s" s;
res
end
@@ -4125,7 +4131,6 @@ let continueUsed () =
| [] -> Kernel.fatal ~current:true "not in a loop"
| (While lr | NotWhile lr) :: _ -> !lr <> ""
-
(****** TYPE SPECIFIERS *******)
(* JS: return [Some s] if the attribute string is the attribute annotation [s]
diff --git a/tests/syntax/attributes-declarations-definitions.c b/tests/syntax/attributes-declarations-definitions.c
index 9c7daac462a..69344179b06 100644
--- a/tests/syntax/attributes-declarations-definitions.c
+++ b/tests/syntax/attributes-declarations-definitions.c
@@ -1,3 +1,8 @@
+/* run.config
+ STDOPT:
+ EXIT: 1
+ STDOPT: #"-cpp-extra-args=-DUNSUPPORTED"
+*/
//@ requires p1 >= 1;
int __attribute__((tret1)) f(int __attribute__((arg1)) p1) __attribute__((f1));
@@ -51,3 +56,8 @@ int __attribute__((o)) one_letter_attribute;
int __attribute__((_n)) one_letter_attribute_with_underscore;
int __attribute__((e_)) one_letter_attribute_with_underscore_after;
+
+#ifdef UNSUPPORTED
+// explicitly unsupported attributes must cause errors
+typedef char V __attribute__((vector_size (64))); // vector_size is unsupported
+#endif
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.0.res.oracle
similarity index 90%
rename from tests/syntax/oracle/attributes-declarations-definitions.res.oracle
rename to tests/syntax/oracle/attributes-declarations-definitions.0.res.oracle
index fb1151fa5ae..8b1788aed0b 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.0.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
-[kernel] attributes-declarations-definitions.c:7: Warning:
- found two contracts (old location: attributes-declarations-definitions.c:1). Merging them
-[kernel] attributes-declarations-definitions.c:16: Warning:
- found two contracts (old location: attributes-declarations-definitions.c:8). Merging them
+[kernel] attributes-declarations-definitions.c:12: Warning:
+ found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
+[kernel] attributes-declarations-definitions.c:21: Warning:
+ found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
/* Generated by Frama-C */
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle
new file mode 100644
index 00000000000..0b83c35f45a
--- /dev/null
+++ b/tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
+[kernel] attributes-declarations-definitions.c:12: Warning:
+ found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
+[kernel] attributes-declarations-definitions.c:21: Warning:
+ found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
+[kernel] attributes-declarations-definitions.c:62: User Error:
+ unsupported attribute: vector_size
+[kernel] User Error: stopping on file "attributes-declarations-definitions.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
--
GitLab