Skip to content

Commit 32af11e

Browse files
Use as_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 as_const. In the example in `jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5` this reduced the number of calls to detach from 744638 to 736844.
1 parent d07fbfb commit 32af11e

File tree

1 file changed

+8
-5
lines changed

1 file changed

+8
-5
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 8 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/as_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(as_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+
as_const(address_of_expr).object().type();
337339
}
338340
else
339341
{
@@ -343,12 +345,13 @@ void goto_symex_statet::rename(
343345
Forall_operands(it, expr)
344346
rename(*it, ns, level);
345347

348+
const exprt &c_expr = as_const(expr);
346349
INVARIANT(
347350
(expr.id() != ID_with ||
348-
expr.type() == to_with_expr(expr).old().type()) &&
351+
c_expr.type() == to_with_expr(c_expr).old().type()) &&
349352
(expr.id() != ID_if ||
350-
(expr.type() == to_if_expr(expr).true_case().type() &&
351-
expr.type() == to_if_expr(expr).false_case().type())),
353+
(c_expr.type() == to_if_expr(c_expr).true_case().type() &&
354+
c_expr.type() == to_if_expr(c_expr).false_case().type())),
352355
"Type of renamed expr should be the same as operands for with_exprt and "
353356
"if_exprt");
354357
}

0 commit comments

Comments
 (0)