Skip to content

Commit 0f1abe1

Browse files
committed
DECL VCCs: don't check non-existent SSA-rhs
DECL clauses do not give an RHS, so comparing its type against the LHS is meaningless (and always fails).
1 parent 5867785 commit 0f1abe1

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/goto-symex/symex_target_equation.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -961,8 +961,12 @@ void symex_target_equationt::SSA_stept::validate(
961961
case goto_trace_stept::typet::CONSTRAINT:
962962
validate_full_expr(cond_expr, ns, vm);
963963
break;
964-
case goto_trace_stept::typet::ASSIGNMENT:
965964
case goto_trace_stept::typet::DECL:
965+
validate_full_expr(ssa_lhs, ns, vm);
966+
validate_full_expr(ssa_full_lhs, ns, vm);
967+
validate_full_expr(original_full_lhs, ns, vm);
968+
break;
969+
case goto_trace_stept::typet::ASSIGNMENT:
966970
validate_full_expr(ssa_lhs, ns, vm);
967971
validate_full_expr(ssa_full_lhs, ns, vm);
968972
validate_full_expr(original_full_lhs, ns, vm);

0 commit comments

Comments
 (0)