UnionDomain: Fix invariant generation for the case an offset is given.

goblint · Oct 14, 2022 · af65ce4 · af65ce4
1 parent e52b3c0
commit af65ce4
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml
@@ -38,12 +38,13 @@ struct
       end
     (* invariant for one field *)
     | Field (f, offset) ->
-      let c_lval = Option.get lval in
       begin match lift_f with
         | `Lifted f' ->
           let v = Values.cast ~torg:f'.ftype f.ftype v in
-          let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
-          value_invariant ~offset ~lval:(Some f_lval) v
+          (* Do not add the field offset to lval here:
+             Otherwise, for pointers to a member type of the union, this would
+             generate an assertion with illegal field offset. *)
+          value_invariant ~offset ~lval:lval v
         | `Top
         | `Bot ->
           Invariant.none