Skip to content

Commit 9d24442

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 2f4cf0e commit 9d24442

File tree

1 file changed

+12
-3
lines changed

1 file changed

+12
-3
lines changed

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ void gdb_value_extractort::analyze_symbol(const irep_idt &symbol_name)
6767

6868
add_assignment(symbol_expr, target_expr);
6969
}
70-
catch(gdb_interaction_exceptiont e)
70+
catch(gdb_interaction_exceptiont &e)
7171
{
7272
throw analysis_exceptiont(e.what());
7373
}
@@ -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)