Skip to content

Commit c143a27

Browse files
author
Remi Delmas
committed
function contracts: allow history variables for typecast and constant expressions.
1 parent 95d8c91 commit c143a27

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/goto-instrument/contracts/contracts.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -562,9 +562,10 @@ void code_contractst::replace_history_parameter(
562562
{
563563
const auto &parameter = to_history_expr(expr, id).expression();
564564

565+
const auto &id = parameter.id();
565566
if(
566-
parameter.id() == ID_dereference || parameter.id() == ID_member ||
567-
parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
567+
id == ID_dereference || id == ID_member || id == ID_symbol ||
568+
id == ID_ptrmember || id == ID_constant || id == ID_typecast)
568569
{
569570
auto it = parameter2history.find(parameter);
570571

0 commit comments

Comments
 (0)