Merge branch 'feature/andre/better-error-c11-keywords' into 'master'

[Parser] improve error message for unsupported C11 keywords

See merge request frama-c/frama-c!3324

src/kernel_internals/parsing/clexer.mll

@@ -238,8 +238,31 @@ let init_lexicon _ =
           let l =
             Seq.fold_left (fun acc c -> convert_char c :: acc) [] seq
           in
-          CST_STRING (List.rev l,loc)))
-    ]
+          CST_STRING (List.rev l,loc)));
+      (* The following C11 tokens are not yet supported, so we provide some
+         helpful error messages. Usage of 'fatal' instead of 'error' below
+         prevents duplicate error messages due to parsing errors. *)
+      ("_Alignas",
+       fun loc ->
+         Kernel.fatal ~source:(fst loc)
+           "_Alignas is currently unsupported by Frama-C.");
+      ("_Alignof",
+       fun loc ->
+         Kernel.fatal ~source:(fst loc)
+           "_Alignof is currently unsupported by Frama-C.");
+      ("_Complex",
+       fun loc ->
+         Kernel.fatal ~source:(fst loc)
+           "_Complex is currently unsupported by Frama-C.");
+      ("_Generic",
+       fun loc ->
+         Kernel.fatal ~source:(fst loc)
+           "_Generic is currently unsupported by Frama-C.");
+      ("_Imaginary",
+       fun loc ->
+         Kernel.fatal ~source:(fst loc)
+           "_Imaginary is currently unsupported by Frama-C.");
+     ]
 
 
 let is_c_keyword s = Hashtbl.mem lexicon s

tests/syntax/c11-keywords.c

+/* run.config
+   EXIT: 1
+   STDOPT: #"-cpp-extra-args=-DALIGNAS"
+   STDOPT: #"-cpp-extra-args=-DALIGNOF"
+   STDOPT: #"-cpp-extra-args=-DCOMPLEX"
+   STDOPT: #"-cpp-extra-args=-DGENERIC"
+   STDOPT: #"-cpp-extra-args=-DIMAGINARY"
+*/
+
+#ifdef ALIGNAS
+struct st_alignas {
+  _Alignas(32) char buf[4];
+};
+#endif
+
+int main(void) {
+#ifdef ALIGNOF
+  int alignd = _Alignof(double);
+#endif
+
+#ifdef COMPLEX
+  double _Complex c = 1;
+#endif
+
+#ifdef GENERIC
+  int generic = _Generic('0', char: 1, int: 2, default: 0);
+#endif
+
+#ifdef IMAGINARY
+  //Note: GCC/Clang do not yet support _Imaginary
+  double _Imaginary im = 0;
+#endif
+
+  return 0;
+}

tests/syntax/oracle/c11-keywords.0.res.oracle

+[kernel] Parsing tests/syntax/c11-keywords.c (with preprocessing)
+[kernel] tests/syntax/c11-keywords.c:12: Failure: 
+  _Alignas is currently unsupported by Frama-C.
+[kernel] User Error: stopping on file "tests/syntax/c11-keywords.c" that has errors. Add
+  '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/c11-keywords.1.res.oracle

+[kernel] Parsing tests/syntax/c11-keywords.c (with preprocessing)
+[kernel] tests/syntax/c11-keywords.c:18: Failure: 
+  _Alignof is currently unsupported by Frama-C.
+[kernel] User Error: stopping on file "tests/syntax/c11-keywords.c" that has errors. Add
+  '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/c11-keywords.2.res.oracle

+[kernel] Parsing tests/syntax/c11-keywords.c (with preprocessing)
+[kernel] tests/syntax/c11-keywords.c:22: Failure: 
+  _Complex is currently unsupported by Frama-C.
+[kernel] User Error: stopping on file "tests/syntax/c11-keywords.c" that has errors. Add
+  '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/c11-keywords.3.res.oracle

+[kernel] Parsing tests/syntax/c11-keywords.c (with preprocessing)
+[kernel] tests/syntax/c11-keywords.c:26: Failure: 
+  _Generic is currently unsupported by Frama-C.
+[kernel] User Error: stopping on file "tests/syntax/c11-keywords.c" that has errors. Add
+  '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/c11-keywords.4.res.oracle

+[kernel] Parsing tests/syntax/c11-keywords.c (with preprocessing)
+[kernel] tests/syntax/c11-keywords.c:31: Failure: 
+  _Imaginary is currently unsupported by Frama-C.
+[kernel] User Error: stopping on file "tests/syntax/c11-keywords.c" that has errors. Add
+  '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.