Skip to content

Commit 9cdb632

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. Also prevents catch-by-value error when compiled with gcc-8.
1 parent fc968f8 commit 9cdb632

File tree

1 file changed

+7
-3
lines changed

1 file changed

+7
-3
lines changed

src/memory-analyzer/analyze_symbol.cpp

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

6969
add_assignment(symbol_expr, target_expr);
7070
}
71-
catch(gdb_interaction_exceptiont e)
71+
catch(gdb_interaction_exceptiont &e)
7272
{
7373
throw analysis_exceptiont(e.what());
7474
}
@@ -248,7 +248,9 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
248248
}
249249
else
250250
{
251-
return it->second;
251+
const symbol_exprt typed_symbol_value = symbol_exprt{
252+
to_symbol_expr(it->second).get_identifier(), expr.type().subtype()};
253+
return typed_symbol_value;
252254
}
253255
}
254256

@@ -304,7 +306,9 @@ exprt gdb_value_extractort::get_pointer_value(
304306
}
305307
else
306308
{
307-
return address_of_exprt(target_expr);
309+
const auto result_expr = address_of_exprt(target_expr);
310+
CHECK_RETURN(result_expr.type() == zero_expr.type());
311+
return result_expr;
308312
}
309313
}
310314
}

0 commit comments

Comments
 (0)