[typing] Take into account tentative defs when merging globals

A tentative def turned into 0-initialization can't be merged with
an explicit definition from another translation unit.

src/kernel_internals/typing/frontc.ml

@@ -41,7 +41,6 @@
 (*                          et Automatique).                                *)
 (****************************************************************************)
 
-
 (* Signal that we are in MS VC mode *) (* BY: never called *)
 let setMSVCMode () =
   Cprint.msvcMode := true

src/kernel_internals/typing/mergecil.ml

@@ -2759,20 +2759,13 @@ let oneFilePass2 (f: file) =
               (H.find emittedVarDefn vi'.vname) in
             (* previously defined; same initializer? *)
             if (equalInitOpts prevInitOpt init.init)
-            || (init.init = None) then (
+            then (
               false  (* do not emit *)
             )
-            else if prevInitOpt = None then (
-              (* The previous occurrence was only a tentative defn. Now,
-                 we have a real one. Set the correct value in the table,
-                 and tell that we need to change the previous into GVarDecl
-              *)
-              H.replace emittedVarDefn vi'.vname(vi',init.init,l);
-              replaceTentativeDefn:=true;
-              true
-            )
             else (
-              (* Both GVars have initializers. *)
+              (* Both GVars have initializers. Note that None in this
+                 context means a tentative definition turned into
+                 a default 0-initialization. *)
               Kernel.error ~current:true
                 "global var %s at %a has different initializer than %a"
                 vi'.vname

tests/syntax/oracle/tentative_definition.0.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x = 1;
+int main(void)
+{
+  return x;
+}
+
+

tests/syntax/oracle/tentative_definition.1.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+extern int x;
+
+int main(void)
+{
+  return x;
+}
+
+

tests/syntax/oracle/tentative_definition.2.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x;
+
+int main(void)
+{
+  return x;
+}
+
+int x = 2;
+

tests/syntax/oracle/tentative_definition.3.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x;
+
+int main(void)
+{
+  return x;
+}
+
+int x;
+

tests/syntax/oracle/tentative_definition.4.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x;
+int main(void)
+{
+  return x;
+}
+
+

tests/syntax/oracle/tentative_definition.5.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/tentative_definition.6.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/tentative_definition.7.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/tentative_definition.8.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/tentative_definition.9.res.oracle

+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/tentative_definition.c

+/* run.config*
+OPT: -cpp-extra-args="-DEEDN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DEENN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENND" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENNN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DNNNN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+EXIT: 1
+OPT: -cpp-extra-args="-DEEDD" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENDD" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENDN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DNNDD" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DNNDN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+*/
+
+// OK (one global defined to 1)
+#ifdef EEDN
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef EENN
+#define LINKAGE_1 extern
+#define DEF_1
+#endif
+
+// OK (one global, initialized to 2)
+#ifdef ENND
+#define LINKAGE_1 extern
+#define DEF_1
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef ENNN
+#define LINKAGE_1 extern
+#define DEF_1
+#endif
+
+// OK-ish (two defs to 0)
+#ifdef NNNN
+#define LINKAGE_1
+#define DEF_1
+#endif
+
+// KO (two conflicting defs)
+#ifdef EEDD
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDD
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDN
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDD
+#define LINKAGE_1
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDN
+#define LINKAGE_1
+#define DEF_1 = 1
+#endif
+
+LINKAGE_1 int x DEF_1;
+
+int main() { return x; }

tests/syntax/tentative_definition_aux.c

+/* run.config*
+DONTRUN: primary test in tentative_definition.c
+*/
+
+#ifdef EEDN
+#define LINKAGE_2 extern
+#define DEF_2
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef EENN
+#define LINKAGE_2 extern
+#define DEF_2
+#endif
+
+// OK (one global, initialized to 2)
+#ifdef ENND
+#define LINKAGE_2
+#define DEF_2 = 2
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef ENNN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+// OK-ish (two defs to 0)
+#ifdef NNNN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+// KO (two conflicting defs)
+#ifdef EEDD
+#define LINKAGE_2 extern
+#define DEF_2 = 2
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDD
+#define LINKAGE_2
+#define DEF_2 = 2
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDD
+#define LINKAGE_2
+#define DEF_2 = 2
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+LINKAGE_2 int x DEF_2;