update for merge

SpencerL-Y · Jul 28, 2024 · e754e5e · e754e5e
1 parent 734fb5c
commit e754e5e
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 3 deletions.
diff --git a/benchmark/case_0.c b/benchmark/case_0.c
@@ -3,8 +3,8 @@
 int main(){
     // int whatever;
     // int * data = malloc(2*sizeof(int));
-    int * data2 = malloc(sizeof(int));  
-    int i = *(data2);
+    int * data2 = malloc(2*sizeof(int));  
+    int i = *(data2 + 1);
     // free(data2);
     // int* j = NULL;
     // int* i = j;

diff --git a/src/goto-symex/dynamic_allocation.cpp b/src/goto-symex/dynamic_allocation.cpp
@@ -114,5 +114,4 @@ void goto_symext::default_replace_dynamic_allocation(expr2tc &expr)
     expr2tc index_expr = index2tc(size_type2(), alloc_arr_2, obj_expr);
     expr = index_expr;
   }
-  // TODO: add slhv dynamic allocation test replacement
 }
diff --git a/src/util/migrate.cpp b/src/util/migrate.cpp
@@ -2657,6 +2657,17 @@ exprt migrate_expr_back(const expr2tc &ref)
     heap_update.set("byte_len", irep_idt(std::to_string(ref2.byte_len)));
     return heap_update;
   }
+  case expr2t::heap_append_id:
+  {
+    const heap_append2t &ref2 = to_heap_append2t(ref);
+    typet thetype = migrate_type_back(ref->type);
+    exprt heap_append("heap_append", thetype);
+    heap_append.copy_to_operands(migrate_expr_back(ref2.src_heap));
+    heap_append.copy_to_operands(migrate_expr_back(ref2.start_addr));
+    heap_append.copy_to_operands(migrate_expr_back(ref2.create_val));
+    heap_append.set("byte_len", irep_idt(std::to_string(ref2.byte_len)));
+    return heap_append;
+  }
   case expr2t::heap_contains_id:
   {
    const heap_contains2t &ref2 = to_heap_contains2t(ref);