Skip to content

Commit c6f6041

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Added evaluation test to gotos
1 parent 1eedc80 commit c6f6041

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/goto-programs/goto_program.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -736,6 +736,7 @@ void goto_programt::instructiont::validate(
736736
evaluates_to_boolean(guard),
737737
"assuming non-boolean condition\n" + guard.pretty(),
738738
source_location);
739+
break;
739740
case ASSERT:
740741
DATA_CHECK_WITH_DIAGNOSTICS(
741742
targets.empty(),
@@ -745,6 +746,13 @@ void goto_programt::instructiont::validate(
745746
evaluates_to_boolean(guard),
746747
"asserting non-boolean condition\n" + guard.pretty(),
747748
source_location);
749+
break;
750+
case GOTO:
751+
DATA_CHECK_WITH_DIAGNOSTICS(
752+
evaluates_to_boolean(guard),
753+
"goto with non-boolean condition\n" + guard.pretty(),
754+
source_location);
755+
break;
748756
default:
749757
break;
750758
}

0 commit comments

Comments
 (0)