Skip to content

Commit 1e354f7

Browse files
author
Remi Delmas
committed
address review comments
1 parent f7ae59e commit 1e354f7

File tree

5 files changed

+40
-35
lines changed

5 files changed

+40
-35
lines changed

‎src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -92,14 +92,14 @@ parse_function_contract_pair(const irep_idt &cli_flag)
9292
else if(split.size() == 2)
9393
{
9494
auto function_name = split[0];
95-
if(function_name.size() == 0)
95+
if(function_name.empty())
9696
{
9797
throw invalid_function_contract_pair_exceptiont{
9898
"couldn't find function name before '/' in '" + cli_flag_str + "'",
9999
correct_format_message};
100100
}
101101
auto contract_name = split[1];
102-
if(contract_name.size() == 0)
102+
if(contract_name.empty())
103103
{
104104
throw invalid_function_contract_pair_exceptiont{
105105
"couldn't find contract name after '/' in '" + cli_flag_str + "'",

‎src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -49,10 +49,11 @@ void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions(
4949
{
5050
for(const auto &expr : assigns_clause)
5151
{
52-
if(can_cast_expr<conditional_target_group_exprt>(expr))
52+
if(
53+
auto target_group =
54+
expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
5355
{
54-
encode_assignable_target_group(
55-
language_mode, to_conditional_target_group_expr(expr), dest);
56+
encode_assignable_target_group(language_mode, *target_group, dest);
5657
}
5758
else
5859
{
@@ -75,10 +76,11 @@ void dfcc_contract_clauses_codegent::gen_spec_frees_instructions(
7576
{
7677
for(const auto &expr : frees_clause)
7778
{
78-
if(can_cast_expr<conditional_target_group_exprt>(expr))
79+
if(
80+
auto target_group =
81+
expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
7982
{
80-
encode_freeable_target_group(
81-
language_mode, to_conditional_target_group_expr(expr), dest);
83+
encode_freeable_target_group(language_mode, *target_group, dest);
8284
}
8385
else
8486
{
@@ -279,10 +281,9 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings(
279281
}
280282

281283
INVARIANT(
282-
recursive_call.size() == 0,
283-
"recursive calls found when inlining goto program");
284+
recursive_call.empty(), "recursive calls found when inlining goto program");
284285

285286
INVARIANT(
286-
not_enough_arguments.size() == 0,
287+
not_enough_arguments.empty(),
287288
"not enough arguments when inlining goto program");
288289
}

‎src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -162,9 +162,9 @@ void dfcc_spec_functionst::generate_havoc_instructions(
162162
if(ins_it->call_function().id() != ID_symbol)
163163
{
164164
throw invalid_source_file_exceptiont(
165-
"Function pointer call '" +
165+
"Function pointer calls are not supported in assigns clauses: '" +
166166
from_expr(ns, function_id, ins_it->call_function()) +
167-
"' in function '" + id2string(function_id) + "' is not supported",
167+
"' called in function '" + id2string(function_id) + "'",
168168
ins_it->source_location());
169169
}
170170

@@ -265,21 +265,25 @@ void dfcc_spec_functionst::to_spec_assigns_function(
265265
.symbol_expr();
266266

267267
to_spec_assigns_instructions(
268-
write_set_to_fill, goto_function.body, nof_targets);
268+
write_set_to_fill,
269+
utils.get_function_symbol(function_id).mode,
270+
goto_function.body,
271+
nof_targets);
269272

270273
goto_model.goto_functions.update();
271274

272275
// instrument for side-effects checking
273276
std::set<irep_idt> function_pointer_contracts;
274277
instrument.instrument_function(function_id, function_pointer_contracts);
275278
INVARIANT(
276-
function_pointer_contracts.size() == 0,
279+
function_pointer_contracts.empty(),
277280
"discovered function pointer contracts unexpectedly");
278281
utils.set_hide(function_id, true);
279282
}
280283

281284
void dfcc_spec_functionst::to_spec_assigns_instructions(
282285
const exprt &write_set_to_fill,
286+
const irep_idt &language_mode,
283287
goto_programt &program,
284288
std::size_t &nof_targets)
285289
{
@@ -295,9 +299,9 @@ void dfcc_spec_functionst::to_spec_assigns_instructions(
295299
if(ins_it->call_function().id() != ID_symbol)
296300
{
297301
throw invalid_source_file_exceptiont(
298-
"Function pointer call '" +
299-
from_expr(ns, "", ins_it->call_function()) +
300-
"' are supported in assigns clauses",
302+
"Function pointer calls are not supported in assigns clauses '" +
303+
from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
304+
"'",
301305
ins_it->source_location());
302306
}
303307

@@ -350,22 +354,26 @@ void dfcc_spec_functionst::to_spec_frees_function(
350354
.symbol_expr();
351355

352356
to_spec_frees_instructions(
353-
write_set_to_fill, goto_function.body, nof_targets);
357+
write_set_to_fill,
358+
utils.get_function_symbol(function_id).mode,
359+
goto_function.body,
360+
nof_targets);
354361

355362
goto_model.goto_functions.update();
356363

357364
// instrument for side-effects checking
358365
std::set<irep_idt> function_pointer_contracts;
359366
instrument.instrument_function(function_id, function_pointer_contracts);
360367
INVARIANT(
361-
function_pointer_contracts.size() == 0,
368+
function_pointer_contracts.empty(),
362369
"discovered function pointer contracts unexpectedly");
363370

364371
utils.set_hide(function_id, true);
365372
}
366373

367374
void dfcc_spec_functionst::to_spec_frees_instructions(
368375
const exprt &write_set_to_fill,
376+
const irep_idt &language_mode,
369377
goto_programt &program,
370378
std::size_t &nof_targets)
371379
{
@@ -378,9 +386,9 @@ void dfcc_spec_functionst::to_spec_frees_instructions(
378386
if(ins_it->call_function().id() != ID_symbol)
379387
{
380388
throw invalid_source_file_exceptiont(
381-
"Function pointer call '" +
382-
from_expr(ns, "", ins_it->call_function()) +
383-
"' are not supported in frees clauses",
389+
"Function pointer calls are not supported in frees clauses: '" +
390+
from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
391+
"'",
384392
ins_it->source_location());
385393
}
386394

‎src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -152,11 +152,13 @@ class dfcc_spec_functionst
152152
/// `__CPROVER_object_from`, `__CPROVER_object_upto`.
153153
///
154154
/// \param[in] write_set_to_fill write set to populate.
155+
/// \param[in] language_mode used to format expressions.
155156
/// \param[inout] program function to transform in place
156157
/// \param[out] nof_targets receives the estimated size of the write set
157158
///
158159
void to_spec_assigns_instructions(
159160
const exprt &write_set_to_fill,
161+
const irep_idt &language_mode,
160162
goto_programt &program,
161163
std::size_t &nof_targets);
162164

@@ -201,11 +203,13 @@ class dfcc_spec_functionst
201203
/// freeable targets: `__CPROVER_freeable`.
202204
///
203205
/// \param[in] write_set_to_fill write set to populate.
206+
/// \param[in] language_mode used to format expressions.
204207
/// \param[inout] program function to transform in place
205208
/// \param[out] nof_targets receives the estimated size of the write set
206209
///
207210
void to_spec_frees_instructions(
208211
const exprt &write_set_to_fill,
212+
const irep_idt &language_mode,
209213
goto_programt &program,
210214
std::size_t &nof_targets);
211215

‎src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,6 @@ Author: Remi Delmas, [email protected]
3030
#include "dfcc_lift_memory_predicates.h"
3131
#include "dfcc_utils.h"
3232

33-
/// Lift a c++ bool to an exprt
34-
static exprt to_bool_expr(bool v)
35-
{
36-
if(v)
37-
return true_exprt();
38-
return false_exprt();
39-
}
40-
4133
/// Generate the contract write set
4234
const symbol_exprt create_contract_write_set(
4335
dfcc_utilst &utils,
@@ -312,8 +304,8 @@ void dfcc_wrapper_programt::encode_requires_write_set()
312304
address_of_write_set,
313305
from_integer(0, size_type()),
314306
from_integer(0, size_type()),
315-
to_bool_expr(check_mode),
316-
to_bool_expr(!check_mode),
307+
make_boolean_expr(check_mode),
308+
make_boolean_expr(!check_mode),
317309
false_exprt(),
318310
false_exprt(),
319311
true_exprt(),
@@ -387,8 +379,8 @@ void dfcc_wrapper_programt::encode_ensures_write_set()
387379
from_integer(0, size_type()),
388380
false_exprt(),
389381
false_exprt(),
390-
to_bool_expr(!check_mode),
391-
to_bool_expr(check_mode),
382+
make_boolean_expr(!check_mode),
383+
make_boolean_expr(check_mode),
392384
true_exprt(),
393385
true_exprt(),
394386
wrapper_sl);

0 commit comments

Comments
 (0)