Merge pull request #1342 from goblint/isssue_1319

Apron: Only replace deref expression with pointed to variable if types coincide

src/analyses/apron/relationAnalysis.apron.ml

@@ -218,10 +218,19 @@ struct
       | Lval (Mem e, NoOffset) ->
         begin match ask (Queries.MayPointTo e) with
           | ad when not (Queries.AD.is_top ad) && (Queries.AD.cardinal ad) = 1 ->
-            begin match Queries.AD.Addr.to_mval (Queries.AD.choose ad) with
-              | Some mval -> ValueDomain.Addr.Mval.to_cil_exp mval
-              | None -> Lval (Mem e, NoOffset)
-            end
+            let replace mval =
+              let pointee = ValueDomain.Addr.Mval.to_cil_exp mval in
+              let pointee_typ = Cil.typeSig @@ Cilfacade.typeOf pointee in
+              let lval_typ = Cil.typeSig @@ Cilfacade.typeOfLval (Mem e, NoOffset) in
+              if pointee_typ = lval_typ then
+                Some pointee
+              else
+                (* there is a type-mismatch between pointee and pointer-type *)
+                (* to avoid mismatch errors, we bail on this expression *)
+                None
+            in
+            let r = Option.bind (Queries.AD.Addr.to_mval (Queries.AD.choose ad)) replace in
+            Option.default (Lval (Mem e, NoOffset)) r
           (* It would be possible to do better here, exploiting e.g. that the things pointed to are known to be equal *)
           (* see: https://github.com/goblint/analyzer/pull/742#discussion_r879099745 *)
           | _ -> Lval (Mem e, NoOffset)

tests/regression/46-apron2/59-issue-1319.c

@@ -0,0 +1,30 @@
+// SKIP PARAM: --enable ana.int.def_exc --enable ana.int.interval --set ana.activated[+] apron
+int other();
+
+int main()
+{
+  unsigned char *t;
+  char c = 'b';
+
+  t = &c;
+
+  // Type of *t and c do not match, this caused a crash before
+  if(*t == 'a') {
+    t++;
+  }
+
+  other();
+}
+
+int other()
+{
+  // Same problem, but a bit more involved
+  unsigned char *t;
+  char buf[100] = "bliblablubapk\r";
+
+  t = buf;
+
+  if(*t == 'a') {
+    t++;
+  }
+}