Skip to content

Commit bd1e41d

Browse files
committed
Add and check type of pointees in memory analyzer
GDB does not know (the CBMC) types but the resulting symbol table requires them. We only do this for non-nil ireps (nil ireps can result from getting pointer values for dynamically allocated memory -- will be addressed in later PRs). Also prevents catch-by-value error when compiled with gcc-8.
1 parent be9d5b1 commit bd1e41d

File tree

1 file changed

+11
-2
lines changed

1 file changed

+11
-2
lines changed

src/memory-analyzer/analyze_symbol.cpp

+11-2
Original file line numberDiff line numberDiff line change
@@ -287,7 +287,14 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
287287
}
288288
else
289289
{
290-
return it->second;
290+
const auto &known_value = it->second;
291+
const auto &expected_type = expr.type().subtype();
292+
if(known_value.is_not_nil() && known_value.type() != expected_type)
293+
{
294+
return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
295+
expected_type};
296+
}
297+
return known_value;
291298
}
292299
}
293300

@@ -340,7 +347,9 @@ exprt gdb_value_extractort::get_pointer_value(
340347
}
341348
else
342349
{
343-
return address_of_exprt(target_expr);
350+
const auto result_expr = address_of_exprt(target_expr);
351+
CHECK_RETURN(result_expr.type() == zero_expr.type());
352+
return result_expr;
344353
}
345354
}
346355
}

0 commit comments

Comments
 (0)