Skip to content

Commit 48c7e91

Browse files
committed
goto-harness: use new symbolt constructors
To the extent possible, apply resource-acquisition-is-initialisation. The constructors ensure that at least the most essential fields (name, type, mode) are set.
1 parent 45a841b commit 48c7e91

File tree

2 files changed

+18
-17
lines changed

2 files changed

+18
-17
lines changed

src/goto-harness/memory_snapshot_harness_generator.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -405,14 +405,13 @@ void memory_snapshot_harness_generatort::generate(
405405

406406
// Create harness function symbol
407407

408-
symbolt harness_function_symbol;
409-
harness_function_symbol.name = harness_function_name;
408+
symbolt harness_function_symbol{
409+
harness_function_name,
410+
code_typet({}, empty_typet()),
411+
called_function_symbol->mode};
410412
harness_function_symbol.base_name = harness_function_name;
411413
harness_function_symbol.pretty_name = harness_function_name;
412-
413414
harness_function_symbol.is_lvalue = true;
414-
harness_function_symbol.mode = called_function_symbol->mode;
415-
harness_function_symbol.type = code_typet({}, empty_typet());
416415
harness_function_symbol.value = harness_function_body;
417416

418417
// Add harness function to goto model and symbol table

src/goto-harness/recursive_initialization.cpp

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -377,12 +377,13 @@ symbol_exprt recursive_initializationt::get_malloc_function()
377377
auto malloc_sym = goto_model.symbol_table.lookup("malloc");
378378
if(malloc_sym == nullptr)
379379
{
380-
symbolt new_malloc_sym;
381-
new_malloc_sym.type = code_typet{code_typet{
382-
{code_typet::parametert{size_type()}}, pointer_type(empty_typet{})}};
383-
new_malloc_sym.name = new_malloc_sym.pretty_name =
384-
new_malloc_sym.base_name = "malloc";
385-
new_malloc_sym.mode = initialization_config.mode;
380+
symbolt new_malloc_sym{
381+
"malloc",
382+
code_typet{
383+
{code_typet::parametert{size_type()}}, pointer_type(empty_typet{})},
384+
initialization_config.mode};
385+
new_malloc_sym.pretty_name = "malloc";
386+
new_malloc_sym.base_name = "malloc";
386387
goto_model.symbol_table.insert(new_malloc_sym);
387388
return new_malloc_sym.symbol_expr();
388389
}
@@ -634,12 +635,13 @@ symbol_exprt recursive_initializationt::get_free_function()
634635
auto free_sym = goto_model.symbol_table.lookup("free");
635636
if(free_sym == nullptr)
636637
{
637-
symbolt new_free_sym;
638-
new_free_sym.type = code_typet{code_typet{
639-
{code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}}};
640-
new_free_sym.name = new_free_sym.pretty_name = new_free_sym.base_name =
641-
"free";
642-
new_free_sym.mode = initialization_config.mode;
638+
symbolt new_free_sym{
639+
"free",
640+
code_typet{
641+
{code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}},
642+
initialization_config.mode};
643+
new_free_sym.pretty_name = "free";
644+
new_free_sym.base_name = "free";
643645
goto_model.symbol_table.insert(new_free_sym);
644646
return new_free_sym.symbol_expr();
645647
}

0 commit comments

Comments
 (0)