Skip to content

Commit 219f11b

Browse files
committed
goto-symex: 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 1578cdc commit 219f11b

File tree

2 files changed

+7
-11
lines changed

2 files changed

+7
-11
lines changed

src/goto-symex/auto_objects.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,11 @@ exprt goto_symext::make_auto_object(const typet &type, statet &state)
2222
dynamic_counter++;
2323

2424
// produce auto-object symbol
25-
symbolt symbol;
25+
irep_idt base_name = "auto_object" + std::to_string(dynamic_counter);
26+
symbolt symbol{"symex::" + id2string(base_name), type, ID_C};
2627

27-
symbol.base_name="auto_object"+std::to_string(dynamic_counter);
28-
symbol.name="symex::"+id2string(symbol.base_name);
28+
symbol.base_name = base_name;
2929
symbol.is_lvalue=true;
30-
symbol.type=type;
31-
symbol.mode=ID_C;
3230

3331
state.symbol_table.add(symbol);
3432

src/goto-symex/symex_builtin_functions.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -158,14 +158,12 @@ void goto_symext::symex_allocate(
158158
}
159159

160160
// value
161-
symbolt value_symbol;
162-
163-
value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
164-
value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
161+
irep_idt base_name = "dynamic_object" + std::to_string(dynamic_counter);
162+
symbolt value_symbol{
163+
SYMEX_DYNAMIC_PREFIX + id2string(base_name), *object_type, mode};
164+
value_symbol.base_name = base_name;
165165
value_symbol.is_lvalue=true;
166-
value_symbol.type = *object_type;
167166
value_symbol.type.set(ID_C_dynamic, true);
168-
value_symbol.mode = mode;
169167

170168
state.symbol_table.add(value_symbol);
171169

0 commit comments

Comments
 (0)