Skip to content

Commit 524d4f6

Browse files
committed
Add and use validation methods in code_assignt
1 parent f97b5db commit 524d4f6

File tree

1 file changed

+35
-6
lines changed

1 file changed

+35
-6
lines changed

src/util/std_code.h

Lines changed: 35 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
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

291320
template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
@@ -301,17 +330,17 @@ inline void validate_expr(const code_assignt & x)
301330
inline 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

309338
inline 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

Comments
 (0)