[conversion] mark static data member as extern

so that they can be defined in one translation unit while the class is
declared multiple times.

convert.ml

@@ -3640,6 +3640,9 @@ and convert_class_component (env, implicits, types, fields, others) meth =
       in
       if is_static typ.qualifier then begin
         let attrs = add_fc_destructor_attr env typ [] in
+        (* we have actually an extern declaration in C sense: its definition
+           might reside in another translation unit. *)
+        let base = SpecStorage EXTERN :: base in
         let name = Convert_env.qualify env name in
         let cname,_= Convert_env.typedef_normalize env name TStandard in
         let cname = Mangling.mangle cname TStandard None in

tests/basic/oracle/aggregate.res.oracle

@@ -4,16 +4,12 @@ Now output intermediate result
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  _frama_c_vmt_header ∈ {0}
   _frama_c_rtti_name_info.name ∈ {{ "A" }}
                          {.base_classes; .number_of_base_classes; .pvmt} ∈
                          {0}
-  _frama_c_vmt[0] ∈ {0}
-  _frama_c_vmt_header ∈ {0}
   _frama_c_rtti_name_info.name ∈ {{ "B" }}
                          {.base_classes; .number_of_base_classes; .pvmt} ∈
                          {0}
-  _frama_c_vmt[0] ∈ {0}
   a[0..1] ∈ {0}
   b[0].x ∈ {7}
    [0].y ∈ {0}
@@ -59,10 +55,8 @@ struct B {
 };
 void A::Dtor(struct A const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void A::Ctor(struct A const *this, int _x, int _y)
 {
@@ -82,10 +76,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "B",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,

tests/basic/oracle/anonymous_struct.res.oracle

@@ -30,10 +30,8 @@ struct anonymous_class_1 {
 struct A {
    struct anonymous_class_1 anonymous_2 ;
 };
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 void A::Ctor(struct A const *this);
 
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =

tests/basic/oracle/array_field.res.oracle

@@ -31,10 +31,8 @@ void *malloc(unsigned int size);
 
 void free(void *ptr);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void ArrayFieldTest::Ctor(struct ArrayFieldTest const *this)
 {

tests/basic/oracle/bitfields.res.oracle

@@ -34,10 +34,8 @@ union anonymous_union_1 {
 struct C {
    union anonymous_union_1 anonymous_3 ;
 };
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid(this); */
 long get_b(struct C *this)
 {

tests/basic/oracle/brace_or_equal_initializer.res.oracle

@@ -29,10 +29,8 @@ struct Foo {
    int c ;
    int t[3] ;
 };
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void Foo::Ctor(struct Foo const *this, int x)
 {

tests/basic/oracle/c_link.res.oracle

@@ -39,10 +39,8 @@ struct Foo *operator=(struct Foo *this, struct Foo *__frama_c_arg_0);
 
 void Foo::Dtor(struct Foo const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void Foo::Ctor(struct Foo const *this)
 {
@@ -76,10 +74,8 @@ void Bar::Ctor(struct Bar const *this, struct Bar const *__frama_c_arg_0);
 
 void Bar::Dtor(struct Bar const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void Bar::Ctor(struct Bar const *this)
 {

tests/basic/oracle/default_args.res.oracle

@@ -30,10 +30,8 @@ void A::Ctor(struct A const *this);
 
 void A::Dtor(struct A const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void A::Ctor(struct A const *this)
 {

tests/basic/oracle/delete_all_kind.res.oracle

@@ -47,10 +47,8 @@ void A::Ctor(struct A const *this);
 
 void A::Dtor(struct A const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 void A::delete(void *ptr)
 {
   return;
@@ -96,10 +94,8 @@ void B::Ctor(struct B const *this);
 
 void B::Dtor(struct B const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void B::Ctor(struct B const *this)
 {

tests/basic/oracle/forWithSimpleDecl.res.oracle

@@ -29,10 +29,8 @@ struct s {
 };
 void s::Ctor(struct s const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void s::Ctor(struct s const *this)
 {

tests/basic/oracle/forward.res.oracle

@@ -29,19 +29,15 @@ struct B {
 struct A {
    int x ;
 };
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "B",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "A",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,

tests/basic/oracle/gnu_body.res.oracle

@@ -30,10 +30,8 @@ int f(int x);
 
 void A::Ctor(struct A const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 int t3(struct A const *this);
 
 int id(struct A const *this, int x);

tests/basic/oracle/incomplete_type.res.oracle

@@ -39,10 +39,8 @@ void A::Ctor(struct A const *this);
 
 void A::Dtor(struct A const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void A::Ctor(struct A const *this)
 {
@@ -62,10 +60,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .pvmt = (struct _frama_c_vmt *)0};
 void B::Ctor(struct B const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 void m_fn1(struct B *this, struct A **p1, long __frama_c_arg_1,
            unsigned int __frama_c_arg_2);
 

tests/basic/oracle/init.res.oracle

@@ -31,19 +31,15 @@ struct myStruct {
    myArray a ;
 };
 typedef struct myStruct myStruct;
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "A",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "myStruct",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,

tests/basic/oracle/method_translation_order_2064.res.oracle

@@ -26,10 +26,8 @@ struct Point;
 struct Point {
    int xx ;
 };
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid(this);
     requires \valid(p); */
 void bar(struct Point *this, struct Point *p)

tests/basic/oracle/namespace.res.oracle

@@ -35,10 +35,8 @@ union anonymous_union_2 {
 struct A {
    union anonymous_union_2 anonymous_1 ;
 };
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 _Bool is_zero(struct A *this);
 
 _Bool is_foo(struct A *this);

tests/basic/oracle/new.res.oracle

@@ -51,10 +51,8 @@ int glob(void)
 
 void Base::Ctor(struct Base const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void Base::Ctor(struct Base const *this)
 {
@@ -68,11 +66,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .pvmt = (struct _frama_c_vmt *)0};
 void A::Ctor(struct A const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
-struct _frama_c_vmt_content _frama_c_vmt[1];
 void *A::new(unsigned int size);
 
 void m_fn2(struct A *this);
@@ -102,10 +97,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .pvmt = (struct _frama_c_vmt *)0};
 void B::Ctor(struct B const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 void *B::new(unsigned int size)
 {
   void *__retres;

tests/basic/oracle/new_all_kind.res.oracle

@@ -33,10 +33,8 @@ struct A {
 };
 void *malloc(unsigned int size);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void A::Ctor(struct A const *this)
 {

tests/basic/oracle/new_array.res.oracle

@@ -49,10 +49,8 @@ int glob(void)
 
 void Base::Ctor(struct Base const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
 void Base::Ctor(struct Base const *this)
 {
@@ -66,11 +64,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .pvmt = (struct _frama_c_vmt *)0};
 void A::Ctor(struct A const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
-struct _frama_c_vmt_content _frama_c_vmt[1];
 void *A::new[](unsigned int size);
 
 void m_fn2(struct A *this);
@@ -109,10 +104,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .pvmt = (struct _frama_c_vmt *)0};
 void B::Ctor(struct B const *this);
 
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 void *B::new[](unsigned int size)
 {
   void *__retres;

tests/basic/oracle/opt.res.oracle

@@ -25,10 +25,8 @@ struct _frama_c_rtti_name_info_node {
 struct option {
    int val ;
 };
-struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-struct _frama_c_vmt_content _frama_c_vmt[1];
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "option",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,