Skip to content

Commit 42bf8fe

Browse files
committed
Add check for well-formedness of assign instructions
1 parent a39be9e commit 42bf8fe

File tree

1 file changed

+16
-2
lines changed

1 file changed

+16
-2
lines changed

src/goto-programs/goto_program.h

+16-2
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,11 @@ Author: Daniel Kroening, [email protected]
2020

2121
#include <util/invariant.h>
2222
#include <util/namespace.h>
23-
#include <util/symbol_table.h>
2423
#include <util/source_location.h>
25-
#include <util/std_expr.h>
2624
#include <util/std_code.h>
25+
#include <util/std_expr.h>
26+
#include <util/symbol_table.h>
27+
#include <util/validate.h>
2728

2829
/// The type of an instruction in a GOTO program.
2930
enum goto_program_instruction_typet
@@ -407,6 +408,19 @@ class goto_programt
407408
{
408409
validate_code_full_pick(code, ns, vm);
409410
validate_expr_full_pick(guard, ns, vm);
411+
412+
switch(type)
413+
{
414+
case ASSIGN:
415+
DATA_CHECK(
416+
code.id() == ID_assign,
417+
"assign instruction should contain an assign statement");
418+
DATA_CHECK(
419+
targets.empty(), "assign instruction should not have a target");
420+
break;
421+
default:
422+
break;
423+
}
410424
}
411425
};
412426

0 commit comments

Comments
 (0)