Skip to content

Commit fc1b588

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 32115b9 commit fc1b588

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
@@ -404,14 +404,13 @@ void memory_snapshot_harness_generatort::generate(
404404

405405
// Create harness function symbol
406406

407-
symbolt harness_function_symbol;
408-
harness_function_symbol.name = harness_function_name;
407+
symbolt harness_function_symbol{
408+
harness_function_name,
409+
code_typet({}, empty_typet()),
410+
called_function_symbol->mode};
409411
harness_function_symbol.base_name = harness_function_name;
410412
harness_function_symbol.pretty_name = harness_function_name;
411-
412413
harness_function_symbol.is_lvalue = true;
413-
harness_function_symbol.mode = called_function_symbol->mode;
414-
harness_function_symbol.type = code_typet({}, empty_typet());
415414
harness_function_symbol.value = harness_function_body;
416415

417416
// 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)