Skip to content

Commit 706c95b

Browse files
committed
Add and use validation methods in code_assignt
1 parent 81a5347 commit 706c95b

File tree

1 file changed

+35
-6
lines changed

1 file changed

+35
-6
lines changed

src/util/std_code.h

+35-6
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"
@@ -261,6 +262,34 @@ class code_assignt:public codet
261262
{
262263
return op1();
263264
}
265+
266+
void check(const validation_modet vm = validation_modet::INVARIANT) const
267+
{
268+
DATA_CHECK(operands().size() == 2, "assignment must have two operands");
269+
}
270+
271+
void validate(
272+
const namespacet &ns,
273+
const validation_modet vm = validation_modet::INVARIANT) const
274+
{
275+
check(vm);
276+
277+
DATA_CHECK(
278+
base_type_eq(lhs().type(), rhs().type(), ns),
279+
"lhs and rhs of assignment must have same type");
280+
}
281+
282+
void validate_full(
283+
const namespacet &ns,
284+
const validation_modet vm = validation_modet::INVARIANT) const
285+
{
286+
for(const exprt &op : operands())
287+
{
288+
validate_expr_full_pick(op, ns, vm);
289+
}
290+
291+
validate(ns, vm);
292+
}
264293
};
265294

266295
template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
@@ -276,17 +305,17 @@ inline void validate_expr(const code_assignt & x)
276305
inline const code_assignt &to_code_assign(const codet &code)
277306
{
278307
PRECONDITION(code.get_statement() == ID_assign);
279-
DATA_INVARIANT(
280-
code.operands().size() == 2, "assignment must have two operands");
281-
return static_cast<const code_assignt &>(code);
308+
const code_assignt &ret = static_cast<const code_assignt &>(code);
309+
ret.check();
310+
return ret;
282311
}
283312

284313
inline code_assignt &to_code_assign(codet &code)
285314
{
286315
PRECONDITION(code.get_statement() == ID_assign);
287-
DATA_INVARIANT(
288-
code.operands().size() == 2, "assignment must have two operands");
289-
return static_cast<code_assignt &>(code);
316+
code_assignt &ret = static_cast<code_assignt &>(code);
317+
ret.check();
318+
return ret;
290319
}
291320

292321
/// A `codet` representing the declaration of a local variable.

0 commit comments

Comments
 (0)