Correctly set value-set dereference pointer

Author: peterschrammel

src/pointer-analysis/value_set_dereference.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
@@ -661,8 +662,21 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     result.pointer = typecast_exprt::conditional_cast(
       address_of_exprt{skip_typecast(o.root_object())}, pointer_type);
 
-    if(!memory_model(result.value, dereference_type, offset, ns))
+    if(memory_model(result.value, dereference_type, offset, ns))
+    {
+      // set pointer correctly
+      result.pointer = typecast_exprt::conditional_cast(
+        plus_exprt(
+          typecast_exprt(
+            result.pointer,
+            pointer_typet(char_type(), pointer_type.get_width())),
+          offset),
+        pointer_type);
+    }
+    else
+    {
       return {}; // give up, no way that this is ok
+    }
 
     return result;
   }