diff --git a/src/kernel_internals/typing/frontc.ml b/src/kernel_internals/typing/frontc.ml index de9fec4dfc3953ad49790bafd1a44c417ba5d6c0..aac0b990d40dc4f934c4418475d6b7263979f9da 100644 --- a/src/kernel_internals/typing/frontc.ml +++ b/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 diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml index 7fe064e19d786945e81b32f6ee274802dcadfd65..0da9d5eabce3540239f66bfa18bb7c2b22953684 100644 --- a/src/kernel_internals/typing/mergecil.ml +++ b/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 diff --git a/tests/syntax/oracle/tentative_definition.0.res.oracle b/tests/syntax/oracle/tentative_definition.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..373498b824a1bc38496b1cef0a4dff7db7a53d3f --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.0.res.oracle @@ -0,0 +1,10 @@ +[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; +} + + diff --git a/tests/syntax/oracle/tentative_definition.1.res.oracle b/tests/syntax/oracle/tentative_definition.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..95d3d686b39d34ea5aa39848603ef10990e0218e --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.1.res.oracle @@ -0,0 +1,11 @@ +[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; +} + + diff --git a/tests/syntax/oracle/tentative_definition.2.res.oracle b/tests/syntax/oracle/tentative_definition.2.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..db0e058c1f0dc431b3e7186ddef9c22c15017865 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.2.res.oracle @@ -0,0 +1,12 @@ +[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; + diff --git a/tests/syntax/oracle/tentative_definition.3.res.oracle b/tests/syntax/oracle/tentative_definition.3.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..c4ca3ded89c557de071e33b73030ca62b8fc2355 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.3.res.oracle @@ -0,0 +1,12 @@ +[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; + diff --git a/tests/syntax/oracle/tentative_definition.4.res.oracle b/tests/syntax/oracle/tentative_definition.4.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..b50717c0eefc2b2d69cc6d8f8351fbeb1fc42466 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.4.res.oracle @@ -0,0 +1,10 @@ +[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; +} + + diff --git a/tests/syntax/oracle/tentative_definition.5.res.oracle b/tests/syntax/oracle/tentative_definition.5.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..14316d7a790372d310751b5d9e0abc75888f56d1 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.5.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/tentative_definition.6.res.oracle b/tests/syntax/oracle/tentative_definition.6.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..14316d7a790372d310751b5d9e0abc75888f56d1 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.6.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/tentative_definition.7.res.oracle b/tests/syntax/oracle/tentative_definition.7.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..14316d7a790372d310751b5d9e0abc75888f56d1 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.7.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/tentative_definition.8.res.oracle b/tests/syntax/oracle/tentative_definition.8.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..14316d7a790372d310751b5d9e0abc75888f56d1 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.8.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/tentative_definition.9.res.oracle b/tests/syntax/oracle/tentative_definition.9.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..14316d7a790372d310751b5d9e0abc75888f56d1 --- /dev/null +++ b/tests/syntax/oracle/tentative_definition.9.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/tentative_definition.c b/tests/syntax/tentative_definition.c new file mode 100644 index 0000000000000000000000000000000000000000..2d8e8726590485e19e0ec48173453ad31bb4f22d --- /dev/null +++ b/tests/syntax/tentative_definition.c @@ -0,0 +1,77 @@ +/* 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; } diff --git a/tests/syntax/tentative_definition_aux.c b/tests/syntax/tentative_definition_aux.c new file mode 100644 index 0000000000000000000000000000000000000000..3a94c22d1404c8e48a5c7efd9bf262ae3c6a04b6 --- /dev/null +++ b/tests/syntax/tentative_definition_aux.c @@ -0,0 +1,64 @@ +/* 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;