diff --git a/tests/libc/check_libc_anonymous_tags.ml b/tests/libc/check_libc_anonymous_tags.ml new file mode 100644 index 0000000000000000000000000000000000000000..62bb754fb908f86bb3bbb7bdb0fc903341eb20f4 --- /dev/null +++ b/tests/libc/check_libc_anonymous_tags.ml @@ -0,0 +1,57 @@ +(* Checks that the Frama-C libc does not declare any anonymous + enums/structs/unions *) + +open Cil_types + +class tags_visitor = object + inherit Visitor.frama_c_inplace + val in_stdlib = ref false + + method! vglob_aux g = + if Cil.hasAttribute "fc_stdlib" (Cil.global_attributes g) then + begin + in_stdlib := true; + begin + match g with + | GEnumTag (ei, loc) | GEnumTagDecl (ei, loc) -> + if ei.eorig_name = "" && !in_stdlib then + Kernel.warning ~source:(fst loc) ~once:true + "anonymous enum in Frama-C stdlib"; + | GCompTag (ci, loc) | GCompTagDecl (ci, loc) -> + if ci.corig_name = "" && !in_stdlib then + Kernel.warning ~source:(fst loc) ~once:true + "anonymous %s in Frama-C stdlib" + (if ci.cstruct then "struct" else "union"); + | _ -> () + end; + Cil.DoChildren + end + else begin + in_stdlib := false; + Cil.SkipChildren + end + + method! vtype typ = + begin + match typ with + | TEnum (ei, _) when ei.eorig_name = "" && !in_stdlib -> + Kernel.warning ~current:true ~once:true + "anonymous enum in Frama-C stdlib"; + () + | TComp (ci, _, _) when ci.corig_name = "" && !in_stdlib -> + Kernel.warning ~current:true ~once:true + "anonymous %s in Frama-C stdlib" + (if ci.cstruct then "struct" else "union") + | _ -> () + end; + Cil.DoChildren +end + +let run_once = ref false + +let () = + Db.Main.extend (fun () -> + if not !run_once then begin + run_once := true; + Visitor.visitFramacFile (new tags_visitor) (Ast.get ()) + end) diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c index 108fa7a3ad4a0cdf546d0127c2aec388f32077ae..fc52ca5ff0ad17a4190b6bb394a20cd090e22d0f 100644 --- a/tests/libc/fc_libc.c +++ b/tests/libc/fc_libc.c @@ -2,10 +2,12 @@ EXECNOW: make -s @PTEST_DIR@/check_libc_naming_conventions.cmxs EXECNOW: make -s @PTEST_DIR@/check_const.cmxs EXECNOW: make -s @PTEST_DIR@/check_parsing_individual_headers.cmxs + EXECNOW: make -s @PTEST_DIR@/check_libc_anonymous_tags.cmxs EXECNOW: make -s @PTEST_DIR@/check_compliance.cmxs OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc OPT: -print -print-libc OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers + OPT: -load-module @PTEST_DIR@/check_libc_anonymous_tags OPT: -load-module @PTEST_DIR@/check_compliance -kernel-msg-key printer:attrs CMD: ./tests/libc/check_full_libc.sh OPT: diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle index 7edeeaacb72c89e076fde32302ba704b09368783..d64ea807afda96b59b16bcca76633b124b9864dc 100644 --- a/tests/libc/oracle/fc_libc.0.res.oracle +++ b/tests/libc/oracle/fc_libc.0.res.oracle @@ -4,10 +4,10 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/libc/fc_libc.c:151: assertion got status valid. -[eva] tests/libc/fc_libc.c:152: assertion got status valid. [eva] tests/libc/fc_libc.c:153: assertion got status valid. [eva] tests/libc/fc_libc.c:154: assertion got status valid. +[eva] tests/libc/fc_libc.c:155: assertion got status valid. +[eva] tests/libc/fc_libc.c:156: assertion got status valid. [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== diff --git a/tests/libc/oracle/fc_libc.3.res.oracle b/tests/libc/oracle/fc_libc.3.res.oracle index 5d4b6982df1e929a36eb1f4f623ad3ca169e8c76..1653140b9190a1d8e1b6e75b8a21068409c46e43 100644 --- a/tests/libc/oracle/fc_libc.3.res.oracle +++ b/tests/libc/oracle/fc_libc.3.res.oracle @@ -1,5 +1 @@ [kernel] Parsing tests/libc/fc_libc.c (with preprocessing) -[kernel] parsing c11_functions.json -[kernel] parsing glibc_functions.json -[kernel] parsing posix_identifiers.json -[kernel] parsing nonstandard_identifiers.json diff --git a/tests/libc/oracle/fc_libc.4.res.oracle b/tests/libc/oracle/fc_libc.4.res.oracle index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..5d4b6982df1e929a36eb1f4f623ad3ca169e8c76 100644 --- a/tests/libc/oracle/fc_libc.4.res.oracle +++ b/tests/libc/oracle/fc_libc.4.res.oracle @@ -0,0 +1,5 @@ +[kernel] Parsing tests/libc/fc_libc.c (with preprocessing) +[kernel] parsing c11_functions.json +[kernel] parsing glibc_functions.json +[kernel] parsing posix_identifiers.json +[kernel] parsing nonstandard_identifiers.json diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391