Skip to content

Commit f6ea3ec

Browse files
committed
Refactor out new_tmp_symbol into utils
1 parent a03d382 commit f6ea3ec

File tree

4 files changed

+49
-36
lines changed

4 files changed

+49
-36
lines changed

src/goto-instrument/contracts/contracts.cpp

Lines changed: 11 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -169,14 +169,16 @@ void code_contractst::check_apply_loop_contracts(
169169
for(const auto &clause : decreases_clause.operands())
170170
{
171171
const auto old_decreases_var =
172-
new_tmp_symbol(clause.type(), loop_head->source_location, mode)
172+
new_tmp_symbol(
173+
clause.type(), loop_head->source_location, mode, symbol_table)
173174
.symbol_expr();
174175
havoc_code.add(
175176
goto_programt::make_decl(old_decreases_var, loop_head->source_location));
176177
old_decreases_vars.push_back(old_decreases_var);
177178

178179
const auto new_decreases_var =
179-
new_tmp_symbol(clause.type(), loop_head->source_location, mode)
180+
new_tmp_symbol(
181+
clause.type(), loop_head->source_location, mode, symbol_table)
180182
.symbol_expr();
181183
havoc_code.add(
182184
goto_programt::make_decl(new_decreases_var, loop_head->source_location));
@@ -317,10 +319,8 @@ void code_contractst::add_quantified_variable(
317319
const auto &quantified_symbol = to_symbol_expr(quantified_variable);
318320

319321
// 1. create fresh symbol
320-
symbolt new_symbol = get_fresh_aux_symbol(
322+
symbolt new_symbol = new_tmp_symbol(
321323
quantified_symbol.type(),
322-
id2string(quantified_symbol.get_identifier()),
323-
"tmp",
324324
quantified_symbol.source_location(),
325325
mode,
326326
symbol_table);
@@ -370,7 +370,8 @@ void code_contractst::replace_history_parameter(
370370
// 1. Create a temporary symbol expression that represents the
371371
// history variable
372372
symbol_exprt tmp_symbol =
373-
new_tmp_symbol(parameter.type(), location, mode).symbol_expr();
373+
new_tmp_symbol(parameter.type(), location, mode, symbol_table)
374+
.symbol_expr();
374375

375376
// 2. Associate the above temporary variable to it's corresponding
376377
// expression
@@ -609,20 +610,6 @@ void code_contractst::apply_loop_contract(
609610
}
610611
}
611612

612-
const symbolt &code_contractst::new_tmp_symbol(
613-
const typet &type,
614-
const source_locationt &source_location,
615-
const irep_idt &mode)
616-
{
617-
return get_fresh_aux_symbol(
618-
type,
619-
id2string(source_location.get_function()) + "::tmp_cc",
620-
"tmp_cc",
621-
source_location,
622-
mode,
623-
symbol_table);
624-
}
625-
626613
symbol_tablet &code_contractst::get_symbol_table()
627614
{
628615
return symbol_table;
@@ -962,7 +949,8 @@ void code_contractst::add_contract_check(
962949
symbol_exprt r = new_tmp_symbol(
963950
code_type.return_type(),
964951
skip->source_location,
965-
function_symbol.mode)
952+
function_symbol.mode,
953+
symbol_table)
966954
.symbol_expr();
967955
check.add(goto_programt::make_decl(r, skip->source_location));
968956

@@ -986,7 +974,8 @@ void code_contractst::add_contract_check(
986974
symbol_exprt p = new_tmp_symbol(
987975
parameter_symbol.type,
988976
skip->source_location,
989-
parameter_symbol.mode)
977+
parameter_symbol.mode,
978+
symbol_table)
990979
.symbol_expr();
991980
check.add(goto_programt::make_decl(p, skip->source_location));
992981
check.add(goto_programt::make_assignment(

src/goto-instrument/contracts/contracts.h

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -96,11 +96,6 @@ class code_contractst
9696

9797
void apply_loop_contracts();
9898

99-
const symbolt &new_tmp_symbol(
100-
const typet &type,
101-
const source_locationt &source_location,
102-
const irep_idt &mode);
103-
10499
void check_apply_loop_contracts(
105100
goto_functionst::goto_functiont &goto_function,
106101
const local_may_aliast &local_may_alias,

src/goto-instrument/contracts/utils.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Date: September 2021
1010

1111
#include "utils.h"
1212

13+
#include <util/fresh_symbol.h>
1314
#include <util/pointer_expr.h>
1415
#include <util/pointer_predicates.h>
1516

@@ -121,3 +122,18 @@ void insert_before_swap_and_advance(
121122
destination.insert_before_swap(target, payload);
122123
std::advance(target, offset);
123124
}
125+
126+
const symbolt &new_tmp_symbol(
127+
const typet &type,
128+
const source_locationt &location,
129+
const irep_idt &mode,
130+
symbol_table_baset &symtab)
131+
{
132+
return get_fresh_aux_symbol(
133+
type,
134+
id2string(location.get_function()) + "::tmp_cc",
135+
"tmp_cc",
136+
location,
137+
mode,
138+
symtab);
139+
}

src/goto-instrument/contracts/utils.h

Lines changed: 22 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -53,10 +53,10 @@ class havoc_if_validt : public havoc_utilst
5353
/// over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ...
5454
/// found in the AST of `expr`.
5555
///
56-
/// \param expr The expression that contains dereferences to be validated
57-
/// \param ns The namespace that defines all symbols appearing in `expr`
56+
/// \param expr: The expression that contains dereferences to be validated.
57+
/// \param ns: The namespace that defines all symbols appearing in `expr`.
5858
/// \return A conjunctive expression that checks validity of all pointers
59-
/// that are dereferenced within `expr`
59+
/// that are dereferenced within `expr`.
6060
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns);
6161

6262
/// \brief Generate a lexicographic less-than comparison over ordered tuples
@@ -65,9 +65,9 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns);
6565
/// comparison, lhs < rhs, between two ordered tuples of variables.
6666
/// This is used in instrumentation of decreases clauses.
6767
///
68-
/// \param lhs A vector of variables representing the LHS of the comparison
69-
/// \param rhs A vector of variables representing the RHS of the comparison
70-
/// \return A lexicographic less-than comparison expression: LHS < RHS
68+
/// \param lhs: A vector of variables representing the LHS of the comparison.
69+
/// \param rhs: A vector of variables representing the RHS of the comparison.
70+
/// \return A lexicographic less-than comparison expression: LHS < RHS.
7171
exprt generate_lexicographic_less_than_check(
7272
const std::vector<symbol_exprt> &lhs,
7373
const std::vector<symbol_exprt> &rhs);
@@ -81,12 +81,25 @@ exprt generate_lexicographic_less_than_check(
8181
/// After insertion, `target` is advanced by the size of the `payload`,
8282
/// and `payload` is destroyed.
8383
///
84-
/// \param destination The destination program for inserting the `payload`
85-
/// \param target The instruction iterator at which to insert the `payload`
86-
/// \param payload The goto program to be inserted into the `destination`
84+
/// \param destination: The destination program for inserting the `payload`.
85+
/// \param target: The instruction iterator at which to insert the `payload`.
86+
/// \param payload: The goto program to be inserted into the `destination`.
8787
void insert_before_swap_and_advance(
8888
goto_programt &destination,
8989
goto_programt::targett &target,
9090
goto_programt &payload);
9191

92+
/// \brief Adds a new temporary symbol to the symbol table.
93+
///
94+
/// \param type: The type of the new symbol.
95+
/// \param location: The source location for the new symbol.
96+
/// \param mode: The mode for the new symbol, e.g. ID_C, ID_java.
97+
/// \param symtab: The symbol table to which the new symbol is to be added.
98+
/// \return The new symbolt object.
99+
const symbolt &new_tmp_symbol(
100+
const typet &type,
101+
const source_locationt &location,
102+
const irep_idt &mode,
103+
symbol_table_baset &symtab);
104+
92105
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H

0 commit comments

Comments
 (0)