Skip to content

Commit 2c2228d

Browse files
Use add_const where relevent in rename
In some places the non const version of .type() and others would be called. We force the const version to be called by using add_const.
1 parent 115baba commit 2c2228d

File tree

1 file changed

+9
-5
lines changed

1 file changed

+9
-5
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <cstdlib>
1515
#include <iostream>
1616

17+
#include <util/add_const.h>
1718
#include <util/base_exceptions.h>
1819
#include <util/exception_utils.h>
1920
#include <util/expr_util.h>
@@ -315,7 +316,7 @@ void goto_symex_statet::rename(
315316
else if(expr.id()==ID_symbol)
316317
{
317318
// we never rename function symbols
318-
if(expr.type().id() == ID_code)
319+
if(add_const(expr).type().id() == ID_code)
319320
{
320321
rename(
321322
expr.type(),
@@ -333,7 +334,8 @@ void goto_symex_statet::rename(
333334
{
334335
auto &address_of_expr = to_address_of_expr(expr);
335336
rename_address(address_of_expr.object(), ns, level);
336-
to_pointer_type(expr.type()).subtype() = address_of_expr.object().type();
337+
to_pointer_type(expr.type()).subtype() =
338+
add_const(address_of_expr).object().type();
337339
}
338340
else
339341
{
@@ -345,10 +347,12 @@ void goto_symex_statet::rename(
345347

346348
INVARIANT(
347349
(expr.id() != ID_with ||
348-
expr.type() == to_with_expr(expr).old().type()) &&
350+
add_const(expr).type() == to_with_expr(add_const(expr)).old().type()) &&
349351
(expr.id() != ID_if ||
350-
(expr.type() == to_if_expr(expr).true_case().type() &&
351-
expr.type() == to_if_expr(expr).false_case().type())),
352+
(add_const(expr).type() ==
353+
to_if_expr(add_const(expr)).true_case().type() &&
354+
add_const(expr).type() ==
355+
to_if_expr(add_const(expr)).false_case().type())),
352356
"Type of renamed expr should be the same as operands for with_exprt and "
353357
"if_exprt");
354358
}

0 commit comments

Comments
 (0)