Merge branch 'fix/union-simpl' into 'stable/titanium'

Do not oversimplify unions

See merge request frama-c/meta!27

meta_simplify.ml

@@ -45,7 +45,11 @@ let neq_lval tl1 tl2 =
   let rec offset_neq o1 o2 = match (o1, o2) with
     | TNoOffset, _  | _, TNoOffset -> false
     | TField (d1, tt1), TField (d2, tt2) ->
-      if d1.forig_name = d2.forig_name then offset_neq tt1 tt2 else true
+      if Cil_datatype.Compinfo.equal d1.fcomp d2.fcomp && d1.fcomp.cstruct then
+        if Cil_datatype.Fieldinfo.equal d1 d2 then
+          offset_neq tt1 tt2
+        else true
+      else false
     | TModel (d1, tt1), TModel (d2, tt2) ->
       if Logic_utils.is_same_model_info d1 d2 then offset_neq tt1 tt2 else true
     | TIndex _, TIndex _ -> false (* Could be improved *)

tests/meta/oracle/simplify.res.oracle

+[kernel] Parsing tests/meta/simplify.c (with preprocessing)
+[meta] Translation is enabled
+[meta] Will process 2 properties
+[meta] Successful translation
+/* Generated by Frama-C */
+union U {
+   int a ;
+   int b ;
+};
+struct S {
+   int a ;
+   int b ;
+};
+struct S s;
+union U u;
+int main(void)
+{
+  int __retres;
+  /*@ assert ssep: meta: \false; */
+  s.a = 42;
+  s.b = 42;
+  /*@ assert usep: meta: \false; */
+  u.a = 42;
+  /*@ assert usep: meta: \separated(&u.b, &u.a); */
+  u.b = 42;
+  __retres = 0;
+  return __retres;
+}
+
+/*@ meta "ssep"; */
+/*@ meta "usep";
+*/
+

tests/meta/simplify.c

+/* run.config
+   OPT: @META@ @PRINT@
+*/
+
+union U {
+    int a, b;
+};
+
+struct S {
+    int a, b;
+};
+
+struct S s;
+union U u;
+
+int main() {
+    s.a = 42;
+    s.b = 42;
+    u.a = 42;
+    u.b = 42;
+}
+
+/*@ meta \prop,
+    \name(ssep),
+    \targets(\ALL),
+    \context(\writing),
+    \separated(\written, &s.a);
+*/
+
+/*@ meta \prop,
+    \name(usep),
+    \targets(\ALL),
+    \context(\writing),
+    \separated(\written, &u.a);
+*/