Skip to content

Commit 7649e74

Browse files
committed
remove symbol initialization from code_declt
DECL instructions in goto programs do not offer the option to initialize the symbol that is declared. This removes the methods for that.
1 parent d15f2b2 commit 7649e74

File tree

1 file changed

+1
-36
lines changed

1 file changed

+1
-36
lines changed

src/util/std_code.h

Lines changed: 1 addition & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -311,47 +311,12 @@ class code_declt:public codet
311311
return symbol().get_identifier();
312312
}
313313

314-
/// Returns the initial value to which the declared variable is initialized,
315-
/// or empty in the case where no initialisation is included.
316-
/// \note: Initial values may be present in the front end but they must be
317-
/// separated into a separate assignment when used in a `goto_instructiont`.
318-
optionalt<exprt> initial_value() const
319-
{
320-
if(operands().size() < 2)
321-
return {};
322-
return {op1()};
323-
}
324-
325-
/// Sets the value to which this declaration initializes the declared
326-
/// variable. Empty optional maybe passed to remove existing initialisation.
327-
/// \note: Initial values may be present in the front end but they must be
328-
/// separated into a separate assignment when used in a `goto_instructiont`.
329-
void set_initial_value(optionalt<exprt> initial_value)
330-
{
331-
if(!initial_value)
332-
{
333-
operands().resize(1);
334-
}
335-
else if(operands().size() < 2)
336-
{
337-
PRECONDITION(operands().size() == 1);
338-
add_to_operands(std::move(*initial_value));
339-
}
340-
else
341-
{
342-
op1() = std::move(*initial_value);
343-
}
344-
}
345-
346314
static void check(
347315
const codet &code,
348316
const validation_modet vm = validation_modet::INVARIANT)
349317
{
350-
// will be size()==1 in the future
351318
DATA_CHECK(
352-
vm,
353-
code.operands().size() >= 1,
354-
"declaration must have one or more operands");
319+
vm, code.operands().size() == 1, "declaration must have one operand");
355320
DATA_CHECK(
356321
vm,
357322
code.op0().id() == ID_symbol,

0 commit comments

Comments
 (0)