Merge pull request #6847 from Herbping/convert_side_effect_with_varia…

…ble_names

associate variables' names to tmp_post

regression/goto-cc-cbmc/tmp_post_with_name/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  char *ptr;
+  ptr = malloc(2);
+  ptr += 2;
+  char c = *ptr++;
+  return 0;
+}

regression/goto-cc-cbmc/tmp_post_with_name/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.pointer_dereference\.5\] line 8 dereference failure: pointer outside object bounds in \*tmp_post_ptr: FAILURE
+\*\* 1 of [0-9]* failed 
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-programs/goto_convert_side_effect.cpp

@@ -314,7 +314,14 @@ void goto_convertt::remove_post(
   if(result_is_used)
   {
     exprt tmp = op;
-    make_temp_symbol(tmp, "post", dest, mode);
+    std::string suffix = "post";
+    if(auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(tmp))
+    {
+      const irep_idt &base_name = ns.lookup(*sym_expr).base_name;
+      suffix += "_" + id2string(base_name);
+    }
+
+    make_temp_symbol(tmp, suffix, dest, mode);
     expr.swap(tmp);
   }
   else