diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 264239138bb9d1bc00fe45a8bac7a0e0fd433de1..3b2e601d3e9c442cae2a372fe53fa3ea888a3332 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 9c7daac462a74b6a5bef1b04b25a5b304a9ed330..69344179b067e9e19eac3c1f2eb3c07f8550a880 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 fb1151fa5ae516f773522f01cf933962bef648c7..8b1788aed0bd7e192a379383c2218fae475bf784 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 0000000000000000000000000000000000000000..0b83c35f45ab5fb43425845f8807646ed441895c --- /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.