1212
1313#include < list>
1414
15+ #include " base_type.h"
1516#include " expr.h"
1617#include " expr_cast.h"
1718#include " invariant.h"
@@ -286,6 +287,34 @@ class code_assignt:public codet
286287 {
287288 return op1 ();
288289 }
290+
291+ void check (const validation_modet vm = validation_modet::INVARIANT) const
292+ {
293+ DATA_CHECK (operands ().size () == 2 , " assignment must have two operands" );
294+ }
295+
296+ void validate (
297+ const namespacet &ns,
298+ const validation_modet vm = validation_modet::INVARIANT) const
299+ {
300+ check (vm);
301+
302+ DATA_CHECK (
303+ base_type_eq (lhs ().type (), rhs ().type (), ns),
304+ " lhs and rhs of assignment must have same type" );
305+ }
306+
307+ void validate_full (
308+ const namespacet &ns,
309+ const validation_modet vm = validation_modet::INVARIANT) const
310+ {
311+ for (const exprt &op : operands ())
312+ {
313+ validate_expr_full_pick (op, ns, vm);
314+ }
315+
316+ validate (ns, vm);
317+ }
289318};
290319
291320template <> inline bool can_cast_expr<code_assignt>(const exprt &base)
@@ -301,17 +330,17 @@ inline void validate_expr(const code_assignt & x)
301330inline const code_assignt &to_code_assign (const codet &code)
302331{
303332 PRECONDITION (code.get_statement () == ID_assign);
304- DATA_INVARIANT (
305- code. operands (). size () == 2 , " assignment must have two operands " );
306- return static_cast < const code_assignt &>(code) ;
333+ const code_assignt &ret = static_cast < const code_assignt &>(code);
334+ ret. check ( );
335+ return ret ;
307336}
308337
309338inline code_assignt &to_code_assign (codet &code)
310339{
311340 PRECONDITION (code.get_statement () == ID_assign);
312- DATA_INVARIANT (
313- code. operands (). size () == 2 , " assignment must have two operands " );
314- return static_cast <code_assignt &>(code) ;
341+ code_assignt &ret = static_cast <code_assignt &>(code);
342+ ret. check ( );
343+ return ret ;
315344}
316345
317346// / A `codet` representing the declaration of a local variable.
0 commit comments