@@ -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