diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 5f20efda92b7434c57284c92debf79d827ef0bcf..ebfddbe38cf7c713ae56f44d57c075a73e07c962 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1564,6 +1564,17 @@ let ignore_vi vi =
let is_ignored_vi vi = Cil_datatype.Varinfo.Set.mem vi !ignored_vi
+let remove_function_statics fdec =
+ let statics =
+ Cil_datatype.Varinfo.Set.of_list (Ast_info.Function.get_statics fdec)
+ in
+ theFile :=
+ List.filter (fun g ->
+ match g with
+ | GVar (vi, _, _) -> not (Cil_datatype.Varinfo.Set.mem vi statics)
+ | _ -> true
+ ) !theFile
+
let oneFilePass1 (f:file) : unit =
H.add fileNames !currentFidx f.fileName;
Kernel.feedback ~dkey:Kernel.dkey_linker
@@ -1577,7 +1588,7 @@ let oneFilePass1 (f:file) : unit =
(* We scan each file and we look at all global varinfo. We see if globals
* with the same name have been encountered before and we merge those types
* *)
- let matchVarinfo (vi: varinfo) (loc, _ as l) =
+ let matchVarinfo ~fromGFun (vi: varinfo) (loc, _ as l) =
ignore (Alpha.registerAlphaName ~alphaTable:vtAlpha
~lookupname:vi.vname ~data:(CurrentLoc.get ()));
(* Make a node for it and put it in vEq *)
@@ -1680,6 +1691,27 @@ let oneFilePass1 (f:file) : unit =
Cil_printer.pp_location oldloc
in
newrep.ndata.vstorage <- newstorage;
+ (* Special handling for 'weak' attributes: since we cannot properly
+ handle the case where the first function definition is to be
+ overridden by the second one, we try to detect whether an old
+ definition had a 'weak' attribute and a later one didn't; in this case,
+ the only way to obtain the "correct" function is to tell the user to
+ invert the order of source files given in the command line.
+ *)
+ if fromGFun && hasAttribute "weak" oldvi.vattr &&
+ not (hasAttribute "weak" vi.vattr) then
+ begin
+ let open Filepath in
+ let oldpath = (fst oldvi.vdecl).pos_path in
+ let newpath = (fst vi.vdecl).pos_path in
+ Kernel.abort ~current:true
+ "weak definition at %a cannot be overridden with \
+ this non-weak definition. @ \
+ Please exchange command-line arguments to put '%a' \
+ before '%a'.@."
+ Printer.pp_location oldvi.vdecl
+ Normalized.pretty newpath Normalized.pretty oldpath
+ end;
newrep.ndata.vattr <- addAttributes oldvi.vattr vi.vattr;
newrep.ndata.vdecl <- newdecl
in
@@ -1689,7 +1721,7 @@ let oneFilePass1 (f:file) : unit =
CurrentLoc.set l;
incr currentDeclIdx;
if vi.vstorage <> Static then begin
- matchVarinfo vi (l, !currentDeclIdx);
+ matchVarinfo ~fromGFun:false vi (l, !currentDeclIdx);
end
| GFun (fdec, l) ->
@@ -1707,7 +1739,7 @@ let oneFilePass1 (f:file) : unit =
fdec.svar.vstorage <- Static;
*)
if fdec.svar.vstorage <> Static then begin
- matchVarinfo fdec.svar (l, !currentDeclIdx)
+ matchVarinfo ~fromGFun:true fdec.svar (l, !currentDeclIdx)
end else begin
if fdec.svar.vinline && mergeInlines then
(* Just create the nodes for inline functions *)
@@ -2828,6 +2860,7 @@ let oneFilePass2 (f: file) =
(mergePushGlobal g');
(H.add emittedFunDefn fdec'.svar.vname (fdec', l, curSum))
| Some (_prevFun, prevLoc, prevSum) ->
+ (* previous was found *)
(* restore old binding for vi, as we are about to drop
the new definition and its formals.
*)
@@ -2836,7 +2869,18 @@ let oneFilePass2 (f: file) =
Some l from getFormalsDecl
in case of a defined function. *)
Cil.setFormals fdec (Option.get defn_formals);
- (* previous was found *)
+ (* Remove static variables (avoids dangling globals in the AST *)
+ remove_function_statics fdec';
+ if hasAttribute "weak" fdec'.svar.vattr then begin
+ Kernel.warning ~current:true ~wkey:Kernel.wkey_linker_weak
+ "dropping weak def'n of func %s at %a in favor of \
+ that at %a"
+ fdec'.svar.vname
+ Cil_printer.pp_location l Cil_printer.pp_location prevLoc;
+ (* We remove the 'weak' attribute, assuming the 'strong'
+ version overrode it. *)
+ fdec'.svar.vattr <- dropAttribute "weak" fdec'.svar.vattr;
+ end else
if (curSum = prevSum) then
Kernel.warning ~current:true
"dropping duplicate def'n of func %s at %a in favor of \
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index fd461ee5e9b4e7ad702a643d28c3fb1c60033299..64b0286d4a82c8f010c03b35e7adfa1fb0c34e82 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -54,17 +54,7 @@ let get_locals f = match f.fundec with
let get_statics f = match f.fundec with
| Definition (d, _) ->
- let statics = ref [] in
- let local_statics_visitor =
- object
- inherit Cil.nopCilVisitor
- method! vblock b =
- statics := !statics @ b.bstatics;
- Cil.DoChildren
- end
- in
- ignore (Cil.visitCilBlock local_statics_visitor d.sbody);
- !statics
+ Ast_info.Function.get_statics d
| Declaration (_, _, _, _) -> []
let () = Globals.get_statics := get_statics
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 2c9418a9254db980617627f9859d20796f8a47db..e1c019546c4378a8da490dfa0968ba58283c4565 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -364,6 +364,22 @@ module Function = struct
let get_name f = (get_vi f).vname
let get_id f = (get_vi f).vid
+ let get_statics fundec =
+ let statics = ref [] in
+ let local_statics_visitor =
+ object
+ inherit Cil.nopCilVisitor
+ method! vblock b =
+ statics := !statics @ b.bstatics;
+ Cil.DoChildren
+ method! vinst _ = Cil.SkipChildren
+ method! vvdec _ = Cil.SkipChildren
+ method! vexpr _ = Cil.SkipChildren
+ end
+ in
+ ignore (Cil.visitCilBlock local_statics_visitor fundec.sbody);
+ !statics
+
end
exception FoundBlock of block
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 36fefd01687ba3d9cdf0081e92fec736355da399..b068cb7fac8bb92949e2f65de23804d936f63c43 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -230,6 +230,10 @@ module Function: sig
val get_vi: cil_function -> varinfo
val get_name: cil_function -> string
val get_id: cil_function -> int
+
+ val get_statics: fundec -> varinfo list
+ (** @since Frama-C+dev *)
+
end
(* ************************************************************************** *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 033d10711adada4534109a640fe36d165223ce94..5b11f4352b8c6e6a627218fb2afcb033c5cb2283 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -156,6 +156,8 @@ let wkey_conditional_feature =
let wkey_drop_unused = register_warn_category "linker:drop-conflicting-unused"
+let wkey_linker_weak = register_warn_category "linker:weak"
+
let wkey_implicit_conv_void_ptr =
register_warn_category "typing:implicit-conv-void-ptr"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 0137185ebb164127c87691936035de9a5de92195..d9142b7318f091c656957404f1f90ad56b0ecedd 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -158,6 +158,8 @@ val wkey_conditional_feature: warn_category
val wkey_drop_unused: warn_category
+val wkey_linker_weak: warn_category
+
val wkey_implicit_conv_void_ptr: warn_category
val wkey_incompatible_types_call: warn_category
diff --git a/tests/misc/mergecil-weak-1.i b/tests/misc/mergecil-weak-1.i
new file mode 100644
index 0000000000000000000000000000000000000000..2a104193c5f03762944d7e08b8222db0d6d6c431
--- /dev/null
+++ b/tests/misc/mergecil-weak-1.i
@@ -0,0 +1,9 @@
+/*run.config
+ DONTRUN: main file is mergecil-weak-3.i
+*/
+
+__attribute__((weak)) int f(void) {
+ int local_var = 1;
+ static int c = 2;
+ return local_var - c;
+}
diff --git a/tests/misc/mergecil-weak-2.i b/tests/misc/mergecil-weak-2.i
new file mode 100644
index 0000000000000000000000000000000000000000..e100eb1df4649f76ff1f2f2b0d1871b88f98a9fa
--- /dev/null
+++ b/tests/misc/mergecil-weak-2.i
@@ -0,0 +1,9 @@
+/*run.config
+ DONTRUN: main file is mergecil-weak-3.i
+*/
+
+int f(void) {
+ int local_var = 1;
+ static int b = 42;
+ return b+local_var;
+}
diff --git a/tests/misc/mergecil-weak-3.i b/tests/misc/mergecil-weak-3.i
new file mode 100644
index 0000000000000000000000000000000000000000..23d0d7b1d17e48a1d6ba4009a3e1bbcb98c4de07
--- /dev/null
+++ b/tests/misc/mergecil-weak-3.i
@@ -0,0 +1,15 @@
+/*run.config
+ OPT: -print %{dep:./mergecil-weak-2.i} %{dep:./mergecil-weak-1.i}
+ OPT: -print %{dep:./mergecil-weak-1.i}
+ OPT: -print %{dep:./mergecil-weak-2.i}
+EXIT: 1
+ OPT: %{dep:./mergecil-weak-1.i} %{dep:./mergecil-weak-2.i}
+*/
+
+int f(void);
+
+int main() {
+ int local_var = 42;
+ int r = f() + f();
+ return r + local_var;
+}
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 8713ec73990faaeb30e877946def34778d502eb9..b80ff7dde480bdca61583ab08da82fa153e10286 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -59,7 +59,7 @@
"annot:multi-from", "annot-error", "asm", "asm:clobber", "audit",
"check", "check:volatile", "cmdline", "file", "ghost",
"ghost:bad-use", "inline", "linker",
- "linker:drop-conflicting-unused", "parser",
+ "linker:drop-conflicting-unused", "linker:weak", "parser",
"parser:conditional-feature", "parser:unnamed-typedef",
"parser:unsupported", "pp", "pp:compilation-db", "pp:line-directive",
"typing", "typing:implicit-conv-void-ptr",
diff --git a/tests/misc/oracle/mergecil-weak-3.0.res.oracle b/tests/misc/oracle/mergecil-weak-3.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a19fb60d008b4f43b9f280456bf14f884fc007e1
--- /dev/null
+++ b/tests/misc/oracle/mergecil-weak-3.0.res.oracle
@@ -0,0 +1,31 @@
+[kernel] Parsing mergecil-weak-3.i (no preprocessing)
+[kernel] Parsing mergecil-weak-2.i (no preprocessing)
+[kernel] Parsing mergecil-weak-1.i (no preprocessing)
+[kernel:linker:weak] mergecil-weak-1.i:5: Warning:
+ dropping weak def'n of func f at mergecil-weak-1.i:5 in favor of that at mergecil-weak-2.i:5
+/* Generated by Frama-C */
+int f(void);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int tmp_0;
+ int local_var = 42;
+ tmp = f();
+ tmp_0 = f();
+ int r = tmp + tmp_0;
+ __retres = r + local_var;
+ return __retres;
+}
+
+static int f_b = 42;
+int f(void)
+{
+ int __retres;
+ int local_var = 1;
+ __retres = f_b + local_var;
+ return __retres;
+}
+
+
diff --git a/tests/misc/oracle/mergecil-weak-3.1.res.oracle b/tests/misc/oracle/mergecil-weak-3.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cf6a880b6dc808c02eca899e318e27547df850af
--- /dev/null
+++ b/tests/misc/oracle/mergecil-weak-3.1.res.oracle
@@ -0,0 +1,29 @@
+[kernel] Parsing mergecil-weak-3.i (no preprocessing)
+[kernel] Parsing mergecil-weak-1.i (no preprocessing)
+/* Generated by Frama-C */
+int f(void) __attribute__((__weak__));
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int tmp_0;
+ int local_var = 42;
+ tmp = f();
+ tmp_0 = f();
+ int r = tmp + tmp_0;
+ __retres = r + local_var;
+ return __retres;
+}
+
+static int f_c = 2;
+int f(void) __attribute__((__weak__));
+int f(void)
+{
+ int __retres;
+ int local_var = 1;
+ __retres = local_var - f_c;
+ return __retres;
+}
+
+
diff --git a/tests/misc/oracle/mergecil-weak-3.2.res.oracle b/tests/misc/oracle/mergecil-weak-3.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..040840382629827879138b41d24ff3c6062adfd6
--- /dev/null
+++ b/tests/misc/oracle/mergecil-weak-3.2.res.oracle
@@ -0,0 +1,28 @@
+[kernel] Parsing mergecil-weak-3.i (no preprocessing)
+[kernel] Parsing mergecil-weak-2.i (no preprocessing)
+/* Generated by Frama-C */
+int f(void);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int tmp_0;
+ int local_var = 42;
+ tmp = f();
+ tmp_0 = f();
+ int r = tmp + tmp_0;
+ __retres = r + local_var;
+ return __retres;
+}
+
+static int f_b = 42;
+int f(void)
+{
+ int __retres;
+ int local_var = 1;
+ __retres = f_b + local_var;
+ return __retres;
+}
+
+
diff --git a/tests/misc/oracle/mergecil-weak-3.3.res.oracle b/tests/misc/oracle/mergecil-weak-3.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..162b6073f4645673e378d7cb9242ba7147a02db0
--- /dev/null
+++ b/tests/misc/oracle/mergecil-weak-3.3.res.oracle
@@ -0,0 +1,7 @@
+[kernel] Parsing mergecil-weak-3.i (no preprocessing)
+[kernel] Parsing mergecil-weak-1.i (no preprocessing)
+[kernel] Parsing mergecil-weak-2.i (no preprocessing)
+[kernel] mergecil-weak-2.i:5: User Error:
+ weak definition at mergecil-weak-3.i:9 cannot be overridden with this non-weak definition.
+ Please exchange command-line arguments to put 'mergecil-weak-2.i' before 'mergecil-weak-3.i'.
+[kernel] Frama-C aborted: invalid user input.