Skip to content

Commit 2b1b8d9

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 78296a2 commit 2b1b8d9

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
@@ -376,12 +376,13 @@ symbol_exprt recursive_initializationt::get_malloc_function()
376376
auto malloc_sym = goto_model.symbol_table.lookup("malloc");
377377
if(malloc_sym == nullptr)
378378
{
379-
symbolt new_malloc_sym;
380-
new_malloc_sym.type = code_typet{code_typet{
381-
{code_typet::parametert{size_type()}}, pointer_type(empty_typet{})}};
382-
new_malloc_sym.name = new_malloc_sym.pretty_name =
383-
new_malloc_sym.base_name = "malloc";
384-
new_malloc_sym.mode = initialization_config.mode;
379+
symbolt new_malloc_sym{
380+
"malloc",
381+
code_typet{
382+
{code_typet::parametert{size_type()}}, pointer_type(empty_typet{})},
383+
initialization_config.mode};
384+
new_malloc_sym.pretty_name = "malloc";
385+
new_malloc_sym.base_name = "malloc";
385386
goto_model.symbol_table.insert(new_malloc_sym);
386387
return new_malloc_sym.symbol_expr();
387388
}
@@ -632,12 +633,13 @@ symbol_exprt recursive_initializationt::get_free_function()
632633
auto free_sym = goto_model.symbol_table.lookup("free");
633634
if(free_sym == nullptr)
634635
{
635-
symbolt new_free_sym;
636-
new_free_sym.type = code_typet{code_typet{
637-
{code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}}};
638-
new_free_sym.name = new_free_sym.pretty_name = new_free_sym.base_name =
639-
"free";
640-
new_free_sym.mode = initialization_config.mode;
636+
symbolt new_free_sym{
637+
"free",
638+
code_typet{
639+
{code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}},
640+
initialization_config.mode};
641+
new_free_sym.pretty_name = "free";
642+
new_free_sym.base_name = "free";
641643
goto_model.symbol_table.insert(new_free_sym);
642644
return new_free_sym.symbol_expr();
643645
}

0 commit comments

Comments
 (0)