@@ -683,24 +683,28 @@ void goto_programt::instructiont::validate(
683
683
case NO_INSTRUCTION_TYPE:
684
684
break ;
685
685
case GOTO:
686
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
686
+ DATA_CHECK_WITH_DIAGNOSTICS (
687
+ vm,
687
688
has_target (),
688
689
" goto instruction expects at least one target" ,
689
690
source_location);
690
691
// get_target checks that targets.size()==1
691
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
692
+ DATA_CHECK_WITH_DIAGNOSTICS (
693
+ vm,
692
694
get_target ()->is_target () && get_target ()->target_number != 0 ,
693
695
" goto target has to be a target" ,
694
696
source_location);
695
697
break ;
696
698
case ASSUME:
697
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
699
+ DATA_CHECK_WITH_DIAGNOSTICS (
700
+ vm,
698
701
targets.empty (),
699
702
" assume instruction should not have a target" ,
700
703
source_location);
701
704
break ;
702
705
case ASSERT:
703
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
706
+ DATA_CHECK_WITH_DIAGNOSTICS (
707
+ vm,
704
708
targets.empty (),
705
709
" assert instruction should not have a target" ,
706
710
source_location);
@@ -722,7 +726,8 @@ void goto_programt::instructiont::validate(
722
726
case ATOMIC_END:
723
727
break ;
724
728
case RETURN:
725
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
729
+ DATA_CHECK_WITH_DIAGNOSTICS (
730
+ vm,
726
731
code.get_statement () == ID_return,
727
732
" return instruction should contain a return statement" ,
728
733
source_location);
@@ -736,29 +741,34 @@ void goto_programt::instructiont::validate(
736
741
vm, targets.empty (), " assign instruction should not have a target" );
737
742
break ;
738
743
case DECL:
739
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
744
+ DATA_CHECK_WITH_DIAGNOSTICS (
745
+ vm,
740
746
code.get_statement () == ID_decl,
741
747
" declaration instructions should contain a declaration statement" ,
742
748
source_location);
743
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
749
+ DATA_CHECK_WITH_DIAGNOSTICS (
750
+ vm,
744
751
!ns.lookup (to_code_decl (code).get_identifier (), table_symbol),
745
752
" declaring unknown symbol: " +
746
753
id2string (to_code_decl (code).get_identifier ()),
747
754
source_location);
748
755
break ;
749
756
case DEAD:
750
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
757
+ DATA_CHECK_WITH_DIAGNOSTICS (
758
+ vm,
751
759
code.get_statement () == ID_dead,
752
760
" dead instructions should contain a dead statement" ,
753
761
source_location);
754
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
762
+ DATA_CHECK_WITH_DIAGNOSTICS (
763
+ vm,
755
764
!ns.lookup (to_code_dead (code).get_identifier (), table_symbol),
756
765
" removing unknown symbol: " +
757
766
id2string (to_code_dead (code).get_identifier ()) + " from scope" ,
758
767
source_location);
759
768
break ;
760
769
case FUNCTION_CALL:
761
- DATA_CHECK_WITH_DIAGNOSTICS (vm,
770
+ DATA_CHECK_WITH_DIAGNOSTICS (
771
+ vm,
762
772
code.get_statement () == ID_function_call,
763
773
" function call instruction should contain a call statement" ,
764
774
source_location);
0 commit comments