From ccef48f2c81f704686164b5a9990034eed7c195c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 8 Mar 2019 15:48:31 +0100
Subject: [PATCH] [typing] Keep trace of all libc includes that contribute to a
var definition
Fixes issue #614
---
src/kernel_internals/typing/cabs2cil.ml | 12 ++++++++++--
src/kernel_internals/typing/mergecil.ml | 11 +++++++++++
src/kernel_services/ast_printing/cil_printer.ml | 4 +---
tests/libc/oracle/fc_libc.0.res.oracle | 6 ++++++
tests/syntax/libc_defs.h | 2 ++
tests/syntax/oracle/libc_defs.res.oracle | 5 +++++
6 files changed, 35 insertions(+), 5 deletions(-)
create mode 100644 tests/syntax/libc_defs.h
create mode 100644 tests/syntax/oracle/libc_defs.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 320b570ab51..6cd61cd0df7 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -325,8 +325,15 @@ let process_stdlib_pragma name args =
let fc_stdlib_attribute attrs =
let s = get_current_stdheader () in
if s = "" then attrs
- else Cil.addAttribute (Attr (fc_stdlib, [AStr s])) attrs
-
+ else begin
+ let payload, attrs =
+ if Cil.hasAttribute fc_stdlib attrs then begin
+ AStr s :: Cil.findAttribute fc_stdlib attrs,
+ Cil.dropAttribute fc_stdlib attrs
+ end else [AStr s], attrs
+ in
+ Cil.addAttribute (Attr (fc_stdlib, payload)) attrs
+ end
(* ICC align/noalign pragmas (not supported by GCC/MSVC with this syntax).
Implemented by translating them to 'aligned' attributes. Currently,
only default and noalign are supported, not explicit alignment values.
@@ -3004,6 +3011,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
(* always favor the location of the definition.*)
oldvi.vdecl <- vi.vdecl;
oldvi.vdefined <- true;
+ oldvi.vattr <- fc_stdlib_attribute oldvi.vattr
end;
(* notice that [vtemp] is immutable, and cannot be updated. Hopefully,
temporaries have sufficiently fresh names that this is not a problem *)
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index ca79f462689..f6b1012b319 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1743,6 +1743,17 @@ let oneFilePass1 (f:file) : unit =
end else Kernel.abort "%s" msg (* Fail if both variables are used. *)
end
in
+ if Cil.hasAttribute "fc_stdlib" oldvi.vattr then begin
+ let attrprm = Cil.findAttribute "fc_stdlib" oldvi.vattr in
+ let attrprm =
+ if Cil.hasAttribute "fc_stdlib" vi.vattr then begin
+ Cil.findAttribute "fc_stdlib" vi.vattr @ attrprm
+ end else attrprm
+ in
+ let attrs = Cil.dropAttribute "fc_stdlib" newrep.ndata.vattr in
+ let attrs = Cil.addAttribute (Attr ("fc_stdlib", attrprm)) attrs in
+ newrep.ndata.vattr <- attrs;
+ end;
newrep.ndata.vdefined <- vi.vdefined || oldvi.vdefined;
newrep.ndata.vreferenced <- vi.vreferenced || oldvi.vreferenced;
(* We do not want to turn non-"const" globals into "const" one. That
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c395c874ff0..c84b8efd2cc 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -109,9 +109,7 @@ let print_std_includes fmt globs =
in
let add_file acc g =
let attrs = Cil_datatype.Global.attr g in
- match Cil.findAttribute "fc_stdlib" attrs with
- | [ arg ] -> extract_file acc arg
- | _ -> acc
+ List.fold_left extract_file acc (Cil.findAttribute "fc_stdlib" attrs)
in
let includes = List.fold_left add_file Datatype.String.Set.empty globs in
let print_one_include s = Format.fprintf fmt "#include \"%s\"@." s in
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 15885d81a20..ea255ba6278 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -190,15 +190,20 @@
#include "alloca.h"
#include "assert.c"
#include "assert.h"
+#include "ctype.c"
#include "ctype.h"
#include "dirent.h"
+#include "errno.c"
#include "errno.h"
#include "fcntl.h"
#include "fenv.c"
#include "fenv.h"
+#include "getopt.c"
#include "getopt.h"
+#include "glob.c"
#include "glob.h"
#include "iconv.h"
+#include "inttypes.c"
#include "inttypes.h"
#include "libgen.h"
#include "locale.c"
@@ -235,6 +240,7 @@
#include "termios.h"
#include "time.h"
#include "unistd.h"
+#include "wchar.c"
#include "wchar.h"
void main(void)
{
diff --git a/tests/syntax/libc_defs.h b/tests/syntax/libc_defs.h
new file mode 100644
index 00000000000..f2c38aa03a6
--- /dev/null
+++ b/tests/syntax/libc_defs.h
@@ -0,0 +1,2 @@
+#include <errno.h>
+#include <errno.c>
diff --git a/tests/syntax/oracle/libc_defs.res.oracle b/tests/syntax/oracle/libc_defs.res.oracle
new file mode 100644
index 00000000000..0705f794ef5
--- /dev/null
+++ b/tests/syntax/oracle/libc_defs.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing tests/syntax/libc_defs.h (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.c"
+#include "errno.h"
+
--
GitLab