From 4263a1a094d219d27d8327f0d1fe081e5c05df9b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 13 Feb 2023 16:46:11 +0100
Subject: [PATCH] [Kernel] deprecate -c11 and enable it by default
---
doc/userman/user-changes.tex | 9 +++--
doc/userman/user-sources.tex | 25 ++++--------
man/frama-c.1 | 6 +--
man/frama-c.1.md | 6 +--
share/analysis-scripts/estimate_difficulty.py | 1 -
share/libc/stdnoreturn.h | 3 --
src/kernel_internals/parsing/clexer.mll | 40 ++++---------------
src/kernel_internals/typing/cabs2cil.ml | 21 +++++-----
.../plugin_entry_points/kernel.ml | 12 +++++-
.../plugin_entry_points/kernel.mli | 3 ++
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 2 +-
src/plugins/e-acsl/tests/bts/issue-eacsl-40.c | 2 +-
src/plugins/variadic/tests/defined/simple.c | 4 +-
tests/libc/stdnoreturn_h.c | 2 +-
tests/rte/invalid_fptr.i | 2 +-
tests/syntax/anonymous_comp_init.i | 2 +-
tests/syntax/bts0769.i | 2 +-
tests/syntax/built.i | 2 +-
tests/syntax/generic.c | 20 +++++-----
tests/syntax/static_assert.c | 4 +-
tests/syntax/thread.i | 2 +-
tests/syntax/type_redef.i | 2 +-
tests/value/volatile.c | 2 +-
23 files changed, 69 insertions(+), 105 deletions(-)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index a278ae6c20a..2c9097889fe 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -3,10 +3,11 @@
This chapter summarizes the changes in this documentation between each \FramaC
release. First we list changes of the last release.
-%\section*{Frama-C+dev}
-%\begin{itemize}
-%\item …
-%\end{itemize}
+\section*{Frama-C+dev}
+\begin{itemize}
+\item \textbf{Normalizing the Source Code:} deprecated option \texttt{-c11}
+ (enabled by default).
+\end{itemize}
\section*{26.0 (Iron)}
\begin{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 42e1bb39238..09b331badf4 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -327,9 +327,6 @@ To ignore this disabling \pragmadef{UNROLL} pragma and force unrolling, the opti
Passing a negative argument to \texttt{-ulevel} will disable unrolling, even
in case of \texttt{UNROLL} pragma.
-
-\item \optiondef{-}{c11} allows the use of some C11 constructs. Currently
-supported are typedefs redefinition.
\end{description}
\section{Incremental parsing} (experimental)\label{sec:incremental-parsing}
@@ -411,8 +408,11 @@ standard library. They are described below.
\section{Compiler and language extensions}\label{sec:extensions}
\FramaC's default behavior is to be fairly strict concerning language features.
-By default, most non-C99 compiler extensions are not accepted, similarly to
-when compiling a program with \verb+gcc -std=c99 -pedantic -pedantic-errors+.
+By default, most C99 and C11 features are accepted\footnote{For more details
+about C99/C11 feature support, see
+Section~\ref{sec:unsupported-iso-c-features}.}, but most non-ISO C compiler
+extensions are not accepted, similarly to when compiling a program with
+\verb+gcc -std=c11 -pedantic -pedantic-errors+.
However, depending on the machine architecture (see option
\optiondef{-}{machdep}, in Section~\ref{sec:normalize}),
@@ -421,24 +421,13 @@ For instance, trying to parse a program containing an empty initializer,
such as \verb+int c[10] = {};+ will result in the following error message:
\begin{verbatim}
-[kernel] user error: empty initializers only allowed for GCC/MSVC
+[kernel] user error: empty initializers only allowed for GCC/MSVC; see option
+ -machdep or run 'frama-c -machdep help' for the list of available machdeps
\end{verbatim}
This means that using a GCC or MSVC machdep (e.g., \verb+-machdep gcc_x86_32+)
will allow the language extension to be accepted by \FramaC.
-Alternatively, some C11 extensions are supported via option \verb+-c11+.
-For instance, the following program is invalid in C99 but valid in C11
-(typedef redefinition): \lstinline|typedef int a; typedef int a;|
-
-The error message given by \FramaC when trying to parse this program will
-indicate the option needed to allow the file to be parsed:
-
-\begin{verbatim}
-[kernel] user error: redefinition of type 'a' in the same scope is only
- allowed in C11 (option -c11).
-\end{verbatim}
-
\section{Standard library (libc)}\label{sec:libc}
\FramaC bundles a C standard library in order to help parse and analyze code
diff --git a/man/frama-c.1 b/man/frama-c.1
index cd42b77afbd..c960811ac63 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -1,6 +1,6 @@
.\" Automatically generated by Pandoc 2.14.0.3
.\"
-.TH "FRAMA-C" "1" "" "2023-02-01" ""
+.TH "FRAMA-C" "1" "" "2023-02-13" ""
.hy
.\"------------------------------------------------------------------------
.\"
@@ -157,10 +157,6 @@ Defaults to yes.
automatically marks contracts generated from asm as valid.
Defaults to no.
.TP
--c11
-enables (partial) C11 compatibility, e.g.\ typedef redefinitions.
-Defaults to no.
-.TP
[-no]-collapse-call-cast
allows implicit cast between the value returned by a function and the
lvalue it is assigned to.
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index d56f5de6055..5b61fc0b5ec 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -1,5 +1,5 @@
---
-title: 'FRAMA-C(1) 2023-02-01'
+title: 'FRAMA-C(1) 2023-02-13'
header-includes:
- |
```{=man}
@@ -142,10 +142,6 @@ syntax. Defaults to yes.
[-no]-asm-contracts-auto-validate
: automatically marks contracts generated from asm as valid. Defaults to no.
--c11
-: enables (partial) C11 compatibility, e.g. typedef redefinitions.
-Defaults to no.
-
[-no]-collapse-call-cast
: allows implicit cast between the value returned by a function and the lvalue
it is assigned to. Otherwise, a temporary variable is used and the cast is made
diff --git a/share/analysis-scripts/estimate_difficulty.py b/share/analysis-scripts/estimate_difficulty.py
index 8de5a907324..7e5af576871 100755
--- a/share/analysis-scripts/estimate_difficulty.py
+++ b/share/analysis-scripts/estimate_difficulty.py
@@ -315,7 +315,6 @@ c11_unsupported = [
"_Alignas",
"_Alignof",
"_Complex",
- "_Generic",
"_Imaginary",
"alignas",
"alignof", # stdalign.h may use these symbols
diff --git a/share/libc/stdnoreturn.h b/share/libc/stdnoreturn.h
index f872fd0dc61..1672207f62a 100644
--- a/share/libc/stdnoreturn.h
+++ b/share/libc/stdnoreturn.h
@@ -24,8 +24,5 @@
// 'noreturn' is an attribute in C++
#ifndef __cpluscplus
-// Note that Frama-C still requires the '-c11' command-line option to parse
-// the _Noreturn keyword. Mere inclusion of this header without the option
-// will not work.
#define noreturn _Noreturn
#endif
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 6f7884616e4..7f3c63f33ae 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -153,24 +153,12 @@ let init_lexicon _ =
end);
("_Noreturn",
fun loc ->
- if Kernel.C11.get () then NORETURN loc
- else begin
- Kernel.(
- warning
- ~wkey:wkey_conditional_feature
- "_Noreturn is a C11 keyword, use -c11 option to enable it");
- IDENT "_Noreturn"
- end);
+ Kernel.(warning ~wkey:wkey_c11 "_Noreturn is a C11 keyword");
+ NORETURN loc);
("_Static_assert",
fun loc ->
- if Kernel.C11.get () then STATIC_ASSERT loc
- else begin
- Kernel.(
- warning
- ~wkey:wkey_conditional_feature
- "_Static_assert is a C11 keyword, use -c11 option to enable it");
- IDENT "_Static_assert"
- end);
+ Kernel.(warning ~wkey:wkey_c11 "_Static_assert is a C11 keyword");
+ STATIC_ASSERT loc);
("__attribute__", fun loc -> ATTRIBUTE loc);
("__attribute", fun loc -> ATTRIBUTE loc);
("__blockattribute__", fun _ -> BLOCKATTRIBUTE);
@@ -218,14 +206,8 @@ let init_lexicon _ =
("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc);
("_Thread_local",
fun loc ->
- if Kernel.C11.get () then THREAD_LOCAL loc
- else begin
- Kernel.(
- warning
- ~wkey:wkey_conditional_feature
- "_Thread_local is a C11 keyword, use -c11 option to enable it");
- IDENT "_Thread_local"
- end);
+ Kernel.(warning ~wkey:wkey_c11 "_Thread_local is a C11 keyword");
+ THREAD_LOCAL loc);
(* We recognize __thread for GCC machdeps *)
("__thread",
fun loc ->
@@ -266,14 +248,8 @@ let init_lexicon _ =
"_Complex is currently unsupported by Frama-C.");
("_Generic",
fun loc ->
- if Kernel.C11.get () then GENERIC loc
- else begin
- Kernel.(
- warning
- ~wkey:wkey_conditional_feature
- "_Generic is a C11 keyword, use -c11 option to enable it");
- IDENT "_Generic"
- end);
+ Kernel.(warning ~wkey:wkey_c11 "_Generic is a C11 keyword");
+ GENERIC loc);
("_Imaginary",
fun loc ->
Kernel.fatal ~source:(fst loc)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f483a6695bb..a39379b1763 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1074,7 +1074,7 @@ let newAlphaName
end
else raise Not_found
in
- if not (Kernel.C11.get () && kind = "type") then
+ if kind <> "type" then
(* in C11, typedefs can be redefined under some conditions (which are
checked in doTypedef); this test catches other kinds of errors, such
as redefined enumeration constants *)
@@ -5594,11 +5594,8 @@ and makeCompType ghost (isstruct: bool)
if n = missingFieldName then begin
match unrollType ftype with
| TComp _ -> begin
- if not (Kernel.C11.get ()) then
- Kernel.warning ~once:true ~current:true
- "unnamed fields are a C11 extension \
- (use %s to avoid this warning)"
- Kernel.C11.name;
+ Kernel.warning ~wkey:Kernel.wkey_c11 ~once:true ~current:true
+ "unnamed fields are a C11 extension";
incr anonCompFieldNameId;
anonCompFieldName ^ (string_of_int !anonCompFieldNameId)
end
@@ -9885,10 +9882,10 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
Previous declaration was at %a"
n Cil_datatype.Location.pretty oldloc
in
- let error_c11_redefinition () =
- Kernel.error ~current:true
- "redefinition of type '%s' in the same scope is only allowed in C11 \
- (option %s).@ Previous declaration was at %a" n Kernel.C11.name
+ let warn_c11_redefinition () =
+ Kernel.warning ~wkey:Kernel.wkey_c11 ~current:true
+ "redefinition of type '%s' in the same scope is only allowed \
+ in C11.@ Previous declaration was at %a" n
Cil_datatype.Location.pretty oldloc
in
(* Tested with GCC+Clang: redefinition of compatible types in same scope:
@@ -9915,7 +9912,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
error_conflicting_types ()
else
(* redeclaration in same scope valid only in C11 *)
- if not (Kernel.C11.get ()) then error_c11_redefinition ()
+ warn_c11_redefinition ()
| _ -> (* because of the compatibility test, this should not happen *)
Kernel.fatal ~current:true "typeinfo.ttype (%a) should be TComp"
Cil_datatype.Typ.pretty typeinfo.ttype
@@ -9923,7 +9920,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
| TEnum _ -> (* GCC/Clang: "conflicting types" *)
error_conflicting_types ()
| _ -> (* redeclaration in same scope valid only in C11 *)
- if not (Kernel.C11.get ()) then error_c11_redefinition ()
+ warn_c11_redefinition ()
end
end
else if declared_in_current_scope ~ghost n then
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index d008d8f7b40..828554c80e3 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -214,6 +214,9 @@ let wkey_unnamed_typedef = register_warn_category "parser:unnamed-typedef"
let wkey_file_not_found = register_warn_category "file:not-found"
let () = set_warn_status wkey_file_not_found Log.Wfeedback
+let wkey_c11 = register_warn_category "c11"
+let () = set_warn_status wkey_c11 Log.Winactive
+
(* ************************************************************************* *)
(** {2 Specialised functors for building kernel parameters} *)
(* ************************************************************************* *)
@@ -1202,9 +1205,16 @@ let () = Parameter_customize.do_not_reset_on_copy ()
module C11 =
False(struct
let option_name = "-c11"
- let help = "allow C11 constructs (experimental; partial support only)"
+ let help = "[DEPRECATED: Use -kernel-warn-key c11 for warnings about usage \
+ of some C11 constructions.] \
+ This option currently has no effect."
let module_name = "C11"
end)
+let () = C11.add_update_hook
+ (fun _old _new -> warning "Option -c11 is deprecated and has no effect. \
+ (enabled by default). \
+ Use -kernel-warn-key c11 for warnings about \
+ usage of some C11 constructions.")
let () = Parameter_customize.set_group parsing
let () = Parameter_customize.do_not_reset_on_copy ()
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 9a652b26832..0c9a85462af 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -211,6 +211,9 @@ val wkey_unnamed_typedef: warn_category
val wkey_file_not_found: warn_category
(** Warnings related to missing files during preprocessing/parsing. *)
+val wkey_c11: warn_category
+(** Warnings related to usage of C11-specific constructions. *)
+
(* ************************************************************************* *)
(** {2 Functors for late option registration} *)
(** Kernel_function-related options cannot be registered in this module:
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index ec919b1aa43..afbb6568c36 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -423,7 +423,7 @@ Options:
-E pass additional arguments to the Frama-C preprocessor
(e.g. -E \"-Iinclude -DMACRO=1\")
-F pass additional options to the Frama-C command line
- (e.g. -F -c11)
+ (e.g. -F \"-verbose 2\")
-o <file> output the generated code to <file> [a.out.frama.c]
-O <file> output the generated executables to <file> [a.out, a.out.e-acsl]
-M maximize memory-related instrumentation
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
index a4496928065..2060c4c0fd1 100644
--- a/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
@@ -11,7 +11,7 @@
COMMENT: The 'LIBS:' line below disables the filter set by E_ACSL_test.ml
LIBS:
LOG: @PTEST_NAME@.out.frama.c
- OPT: @GLOBAL@ @EACSL@ -cpp-extra-args="-DNO_FCLOSE" -c11 -no-frama-c-stdlib -then-last -print -ocode @PTEST_NAME@.out.frama.c
+ OPT: @GLOBAL@ @EACSL@ -cpp-extra-args="-DNO_FCLOSE" -no-frama-c-stdlib -then-last -print -ocode @PTEST_NAME@.out.frama.c
ENABLED_IF: %{bin-available:gcc}
EXECNOW: BIN @PTEST_NAME@.o gcc -Wno-attributes %{dep:@PTEST_NAME@.out.frama.c} -c -o @PTEST_NAME@.o >@DEV_NULL@ 2>@DEV_NULL@
*/
diff --git a/src/plugins/variadic/tests/defined/simple.c b/src/plugins/variadic/tests/defined/simple.c
index 617d61e4380..542544b6882 100644
--- a/src/plugins/variadic/tests/defined/simple.c
+++ b/src/plugins/variadic/tests/defined/simple.c
@@ -1,6 +1,6 @@
/* run.config
-STDOPT: #"-c11"
-STDOPT: #"-no-frama-c-stdlib -no-pp-annot -c11"
+STDOPT:
+STDOPT: #"-no-frama-c-stdlib -no-pp-annot"
*/
/* The defines and typedefs below avoid issues with Musl: without them,
diff --git a/tests/libc/stdnoreturn_h.c b/tests/libc/stdnoreturn_h.c
index 8b234faea6a..d6d8c9ba6d8 100644
--- a/tests/libc/stdnoreturn_h.c
+++ b/tests/libc/stdnoreturn_h.c
@@ -1,5 +1,5 @@
/*run.config
- STDOPT: #"-c11"
+ STDOPT:
*/
#include <stdnoreturn.h>
diff --git a/tests/rte/invalid_fptr.i b/tests/rte/invalid_fptr.i
index 5321e177f81..b159bf10df3 100644
--- a/tests/rte/invalid_fptr.i
+++ b/tests/rte/invalid_fptr.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-c11 -warn-invalid-pointer -print"
+STDOPT: +"-warn-invalid-pointer -print"
*/
struct S { void (*f)(void); } s;
diff --git a/tests/syntax/anonymous_comp_init.i b/tests/syntax/anonymous_comp_init.i
index b156916cb4e..96fa6bbc6b3 100644
--- a/tests/syntax/anonymous_comp_init.i
+++ b/tests/syntax/anonymous_comp_init.i
@@ -1,5 +1,5 @@
/*run.config
- STDOPT: #"-c11"
+ STDOPT:
*/
typedef struct {
diff --git a/tests/syntax/bts0769.i b/tests/syntax/bts0769.i
index b38d53a6b20..baa5480162a 100644
--- a/tests/syntax/bts0769.i
+++ b/tests/syntax/bts0769.i
@@ -1,5 +1,5 @@
/*run.config
- STDOPT: #"-c11"
+ STDOPT:
*/
struct s {
diff --git a/tests/syntax/built.i b/tests/syntax/built.i
index f8eaf83db71..25023c3bbc6 100644
--- a/tests/syntax/built.i
+++ b/tests/syntax/built.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-machdep gcc_x86_32 -c11"
+STDOPT: +"-machdep gcc_x86_32"
*/
extern __attribute__((const, noreturn))
diff --git a/tests/syntax/generic.c b/tests/syntax/generic.c
index 3b504777f36..17726aab534 100644
--- a/tests/syntax/generic.c
+++ b/tests/syntax/generic.c
@@ -1,16 +1,16 @@
/* run.config
EXIT: 1
- STDOPT:
- STDOPT: #"-c11 -cpp-extra-args=-DNONE"
- STDOPT: #"-c11 -cpp-extra-args=-DTOO_MANY_DEFAULTS"
- STDOPT: #"-c11 -cpp-extra-args=-DTOO_MANY_COMPATIBLE"
- STDOPT: #"-c11 -cpp-extra-args=-DTOO_MANY_COMPATIBLE2"
- STDOPT: #"-c11 -cpp-extra-args=-DTOO_MANY_COMPATIBLE3"
- STDOPT: #"-c11 -cpp-extra-args=-DINCOMPLETE_TYPE"
- STDOPT: #"-c11 -cpp-extra-args=-DINCOMPATIBLE_QUALIFIED_TYPE"
- STDOPT: #"-c11 -cpp-extra-args=-DFUNCTION_TYPE"
+ STDOPT: #"-kernel-warn-key=c11=abort"
+ STDOPT: #"-cpp-extra-args=-DNONE"
+ STDOPT: #"-cpp-extra-args=-DTOO_MANY_DEFAULTS"
+ STDOPT: #"-cpp-extra-args=-DTOO_MANY_COMPATIBLE"
+ STDOPT: #"-cpp-extra-args=-DTOO_MANY_COMPATIBLE2"
+ STDOPT: #"-cpp-extra-args=-DTOO_MANY_COMPATIBLE3"
+ STDOPT: #"-cpp-extra-args=-DINCOMPLETE_TYPE"
+ STDOPT: #"-cpp-extra-args=-DINCOMPATIBLE_QUALIFIED_TYPE"
+ STDOPT: #"-cpp-extra-args=-DFUNCTION_TYPE"
EXIT: 0
- STDOPT: #"-c11"
+ STDOPT:
*/
// Some tests inspired by llvm/clang/test/Sema/generic-selection.c
diff --git a/tests/syntax/static_assert.c b/tests/syntax/static_assert.c
index 93ca57c958c..96821ed7fa9 100644
--- a/tests/syntax/static_assert.c
+++ b/tests/syntax/static_assert.c
@@ -1,7 +1,7 @@
/* run.config
- STDOPT: #"-c11"
+ STDOPT: #""
EXIT: 1
- STDOPT: #"-c11 -cpp-extra-args=-DFAIL"
+ STDOPT: #"-cpp-extra-args=-DFAIL"
*/
_Static_assert(1, "string");
diff --git a/tests/syntax/thread.i b/tests/syntax/thread.i
index 9cbb1501457..495f177b0f0 100644
--- a/tests/syntax/thread.i
+++ b/tests/syntax/thread.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-machdep gcc_x86_32 -c11"
+ STDOPT: +"-machdep gcc_x86_32"
*/
__thread int a;
diff --git a/tests/syntax/type_redef.i b/tests/syntax/type_redef.i
index 2c56c35150b..5b4415aaacf 100644
--- a/tests/syntax/type_redef.i
+++ b/tests/syntax/type_redef.i
@@ -1,7 +1,7 @@
/* run.config
EXIT: 1
STDOPT:
- STDOPT: #"-c11"
+
*/ // Note: redefinition of local typedefs is currently unsupported
typedef int myint;
typedef int myint; //valid in C11 only
diff --git a/tests/value/volatile.c b/tests/value/volatile.c
index 300df2f38b8..c9eccd0e973 100644
--- a/tests/value/volatile.c
+++ b/tests/value/volatile.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-no-deps -no-input -no-out -eva-initialization-padding-globals maybe -c11"
+ STDOPT: +"-no-deps -no-input -no-out -eva-initialization-padding-globals maybe"
*/
int volatile G = 1;
--
GitLab