Skip to content

Commit 1697688

Browse files
committed
[Refactor] Rename pointer_size_mapt to type_size_mapt in convert_expr_to_smt
1 parent 658672c commit 1697688

File tree

3 files changed

+6
-6
lines changed

3 files changed

+6
-6
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -588,7 +588,7 @@ static optionalt<smt_termt> try_relational_conversion(
588588
static smt_termt convert_expr_to_smt(
589589
const plus_exprt &plus,
590590
const sub_expression_mapt &converted,
591-
const pointer_size_mapt &pointer_sizes)
591+
const type_size_mapt &pointer_sizes)
592592
{
593593
if(std::all_of(
594594
plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
@@ -638,7 +638,7 @@ static smt_termt convert_expr_to_smt(
638638
static smt_termt convert_expr_to_smt(
639639
const minus_exprt &minus,
640640
const sub_expression_mapt &converted,
641-
const pointer_size_mapt &pointer_sizes)
641+
const type_size_mapt &pointer_sizes)
642642
{
643643
const bool both_operands_bitvector =
644644
can_cast_type<integer_bitvector_typet>(minus.lhs().type()) &&
@@ -1364,7 +1364,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
13641364
const exprt &expr,
13651365
const sub_expression_mapt &converted,
13661366
const smt_object_mapt &object_map,
1367-
const pointer_size_mapt &pointer_sizes,
1367+
const type_size_mapt &pointer_sizes,
13681368
const smt_object_sizet::make_applicationt &call_object_size)
13691369
{
13701370
if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
@@ -1724,7 +1724,7 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
17241724
smt_termt convert_expr_to_smt(
17251725
const exprt &expr,
17261726
const smt_object_mapt &object_map,
1727-
const pointer_size_mapt &pointer_sizes,
1727+
const type_size_mapt &pointer_sizes,
17281728
const smt_object_sizet::make_applicationt &object_size)
17291729
{
17301730
#ifndef CPROVER_INVARIANT_DO_NOT_CHECK

src/solvers/smt2_incremental/convert_expr_to_smt.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ smt_sortt convert_type_to_smt_sort(const typet &type);
2121
smt_termt convert_expr_to_smt(
2222
const exprt &expression,
2323
const smt_object_mapt &object_map,
24-
const pointer_size_mapt &pointer_sizes,
24+
const type_size_mapt &pointer_sizes,
2525
const smt_object_sizet::make_applicationt &object_size);
2626

2727
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ class smt2_incremental_decision_proceduret final
9090
smt_object_mapt object_map;
9191
std::vector<bool> object_size_defined;
9292
smt_object_sizet object_size_function;
93-
pointer_size_mapt pointer_sizes_map;
93+
type_size_mapt pointer_sizes_map;
9494
};
9595

9696
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

0 commit comments

Comments
 (0)