From 414d48533d1f632b98d04d290aee3c67273b3f6c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 26 Jul 2019 18:11:31 +0200
Subject: [PATCH] [Libc] add check for anonymous enums/structs/unions
This check will only be fully operational when rmtmps becomes optional,
but it still protects against errors in used definitions.
---
tests/libc/check_libc_anonymous_tags.ml | 57 +++++++++++++++++++++++++
tests/libc/fc_libc.c | 2 +
tests/libc/oracle/fc_libc.0.res.oracle | 4 +-
tests/libc/oracle/fc_libc.3.res.oracle | 4 --
tests/libc/oracle/fc_libc.4.res.oracle | 5 +++
tests/libc/oracle/fc_libc.5.res.oracle | 0
6 files changed, 66 insertions(+), 6 deletions(-)
create mode 100644 tests/libc/check_libc_anonymous_tags.ml
create mode 100644 tests/libc/oracle/fc_libc.5.res.oracle
diff --git a/tests/libc/check_libc_anonymous_tags.ml b/tests/libc/check_libc_anonymous_tags.ml
new file mode 100644
index 00000000000..62bb754fb90
--- /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 108fa7a3ad4..fc52ca5ff0a 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 7edeeaacb72..d64ea807afd 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 5d4b6982df1..1653140b919 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 e69de29bb2d..5d4b6982df1 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 00000000000..e69de29bb2d
--
GitLab