Skip to content

Commit e3e90ec

Browse files
Petr BauchPetr Bauch
authored andcommitted
Fix doxygen and avoid uninitialized symbol_exprt
For func_init_done_var: now it only lives inside `generate`.
1 parent 1835592 commit e3e90ec

File tree

2 files changed

+15
-12
lines changed

2 files changed

+15
-12
lines changed

src/goto-harness/memory_snapshot_harness_generator.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,7 @@ void memory_snapshot_harness_generatort::validate_options(
101101
}
102102

103103
void memory_snapshot_harness_generatort::add_init_section(
104+
const symbol_exprt &func_init_done_var,
104105
goto_modelt &goto_model) const
105106
{
106107
goto_functionst &goto_functions = goto_model.goto_functions;
@@ -153,9 +154,6 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
153154
recursive_initialization.initialize(symbol.symbol_expr(), 0, {}, code);
154155
}
155156
}
156-
157-
code.add(code_assignt{func_init_done_var, false_exprt{}});
158-
159157
return code;
160158
}
161159

@@ -269,13 +267,15 @@ void memory_snapshot_harness_generatort::generate(
269267
symbol_table);
270268
func_init_done_symbol.is_static_lifetime = true;
271269
func_init_done_symbol.value = false_exprt();
272-
func_init_done_var = func_init_done_symbol.symbol_expr();
270+
symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr();
273271

274-
add_init_section(goto_model);
272+
add_init_section(func_init_done_var, goto_model);
275273

276274
code_blockt harness_function_body =
277275
add_assignments_to_globals(snapshot, goto_model);
278276

277+
harness_function_body.add(code_assignt{func_init_done_var, false_exprt{}});
278+
279279
add_call_with_nondet_arguments(
280280
*called_function_symbol, harness_function_body);
281281

src/goto-harness/memory_snapshot_harness_generator.h

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -97,8 +97,8 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
9797
const goto_programt::instructionst &instructions) const;
9898
};
9999

100-
/// Parse a command line option to extract the user specified \ref
101-
/// entry_goto_locationt
100+
/// Parse a command line option to extract the user specified entry goto
101+
/// location
102102
/// \param cmdl_option: a string of the format <func[:<n>]>
103103
/// \return correctly constructed entry goto location
104104
entry_goto_locationt parse_goto_location(const std::string &cmdl_option);
@@ -124,8 +124,8 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
124124
const goto_programt::instructionst &instructions) const;
125125
};
126126

127-
/// Parse a command line option to extract the user specified \ref
128-
/// entry_source_locationt
127+
/// Parse a command line option to extract the user specified entry source
128+
/// location
129129
/// \param cmdl_option: a string of the format <file:n>
130130
/// \return correctly constructed entry source location
131131
entry_source_locationt parse_source_location(const std::string &cmdl_option);
@@ -158,7 +158,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
158158

159159
/// Find and return the entry instruction (requested by the user as source
160160
/// location: file name + line number)
161-
/// \param entry_goto_location: user specified goto location
161+
/// \param entry_source_location: user specified goto location
162162
/// \param goto_functions: goto functions to be searched for the entry
163163
/// instruction
164164
/// \return the correctly constructed entry location
@@ -214,8 +214,12 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
214214
/// ..second_part..
215215
/// }
216216
///
217+
/// \param func_init_done_var: symbol expression for the `func_init_done`
218+
/// variable
217219
/// \param goto_model: Model where the modification takes place
218-
void add_init_section(goto_modelt &goto_model) const;
220+
void add_init_section(
221+
const symbol_exprt &func_init_done_var,
222+
goto_modelt &goto_model) const;
219223

220224
/// For each global symbol in the \p snapshot symbol table either:
221225
/// 1) add \ref code_assignt assigning a value from the \p snapshot to the
@@ -254,7 +258,6 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
254258

255259
/// data to initialize the entry function
256260
entry_locationt entry_location;
257-
symbol_exprt func_init_done_var;
258261

259262
message_handlert &message_handler;
260263
};

0 commit comments

Comments
 (0)