Enable more assertion in a regression test

by not converting a pointer-to-non-char to it's subtype in case it was
dynamically allocated. Also add a few more checks.

Author: petr-bauch

regression/snapshot-harness/pointer-to-array-int/main.c

@@ -33,12 +33,10 @@ int main()
   assert(first == second);
   // The following assertions will be check in the following PR once
   // dynamically allocated snapshots are properly implemented.
-  /* assert(array_size >= prefix_size); */
-  /* assert(prefix_size >= 0); */
-  /* assert(second[prefix_size] != 6); */
-  /* assert(second[4] == 4); */
+  assert(array_size >= prefix_size);
+  assert(prefix_size >= 0);
+  assert(second[prefix_size] != 6);
+  assert(second[4] == 4);
 
-  /* for(int i = 0; i < prefix_size; i++) */
-  /*   assert(second[i] != prefix[i]); */
   return 0;
 }

src/memory-analyzer/analyze_symbol.cpp

@@ -387,6 +387,7 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
       // add assignment of value to newly created symbol
       add_assignment(array_symbol, new_array);
       values[memory_location] = array_symbol;
+      CHECK_RETURN(array_symbol.type().id() == ID_array);
       return array_symbol;
     }
 
@@ -409,6 +410,8 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
   {
     const auto &known_value = it->second;
     const auto &expected_type = expr.type().subtype();
+    if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
+      return known_value;
     if(known_value.is_not_nil() && known_value.type() != expected_type)
     {
       return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
@@ -500,7 +503,10 @@ exprt gdb_value_extractort::get_pointer_value(
       const auto result_indexed_expr = get_subexpression_at_offset(
         target_expr, 0, zero_expr.type().subtype(), ns);
       CHECK_RETURN(result_indexed_expr.has_value());
+      if(result_indexed_expr->type() == zero_expr.type())
+        return *result_indexed_expr;
       const auto result_expr = address_of_exprt{*result_indexed_expr};
+      CHECK_RETURN(result_expr.type() == zero_expr.type());
       return result_expr;
     }