Skip to content

Commit 14757e2

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Fix pre-pending a expr type check
1 parent 967804f commit 14757e2

File tree

1 file changed

+5
-8
lines changed

1 file changed

+5
-8
lines changed

src/goto-programs/goto_program.cpp

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -676,24 +676,21 @@ void goto_programt::instructiont::validate(
676676
validate_expr_full_pick(guard, ns, vm);
677677

678678
auto evaluates_to_boolean = [](const exprt &e) -> bool {
679-
//typecast to Boolean
679+
if(e.type().id() != ID_bool)
680+
return false;
681+
680682
if(e.id() == ID_typecast)
681683
return e.type().id() == ID_bool;
682684

683685
//Boolean constants
684686
if(e.id() == ID_true || e.id() == ID_false)
685687
return true;
686-
if(e.id() == ID_constant && e.type().id() == ID_bool)
688+
if(e.id() == ID_constant)
687689
return true;
688690

689691
//Symbols
690692
if(e.id() == ID_symbol)
691-
{
692-
if(e.type().id() == ID_code) //function call
693-
return to_code_type(e.type()).return_type().id() == ID_bool;
694-
else //Boolean variable
695-
return e.type().id() == ID_bool;
696-
}
693+
return true;
697694

698695
//arithmetic relations
699696
if(e.id() == ID_equal || e.id() == ID_notequal)

0 commit comments

Comments
 (0)