Skip to content

Commit da85771

Browse files
author
Remi Delmas
committed
CONTRACTS: new c++ methods to build calls to cprover_contracts library
1 parent 6c5b2a6 commit da85771

File tree

5 files changed

+587
-249
lines changed

5 files changed

+587
-249
lines changed

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

+24-46
Original file line numberDiff line numberDiff line change
@@ -521,9 +521,8 @@ void dfcc_instrumentt::insert_add_decl_call(
521521
utils.make_null_check_expr(write_set), target->source_location()));
522522

523523
payload.add(goto_programt::make_function_call(
524-
code_function_callt{
525-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_DECL].symbol_expr(),
526-
{write_set, address_of_exprt(symbol_expr)}},
524+
library.write_set_add_decl_call(
525+
write_set, address_of_exprt(symbol_expr), target->source_location()),
527526
target->source_location()));
528527

529528
auto label_instruction =
@@ -569,9 +568,8 @@ void dfcc_instrumentt::insert_record_dead_call(
569568
utils.make_null_check_expr(write_set), target->source_location()));
570569

571570
payload.add(goto_programt::make_function_call(
572-
code_function_callt{
573-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEAD].symbol_expr(),
574-
{write_set, address_of_exprt(symbol_expr)}},
571+
library.write_set_record_dead_call(
572+
write_set, address_of_exprt(symbol_expr), target->source_location()),
575573
target->source_location()));
576574

577575
auto label_instruction =
@@ -716,14 +714,13 @@ void dfcc_instrumentt::instrument_lhs(
716714
payload.add(goto_programt::make_decl(check_var, lhs_source_location));
717715

718716
payload.add(goto_programt::make_function_call(
719-
code_function_callt{
717+
library.write_set_check_assignment_call(
720718
check_var,
721-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT]
722-
.symbol_expr(),
723-
{write_set,
724-
typecast_exprt::conditional_cast(
725-
address_of_exprt(lhs), pointer_type(empty_typet{})),
726-
utils.make_sizeof_expr(lhs)}},
719+
write_set,
720+
typecast_exprt::conditional_cast(
721+
address_of_exprt(lhs), pointer_type(empty_typet{})),
722+
utils.make_sizeof_expr(lhs),
723+
lhs_source_location),
727724
lhs_source_location));
728725

729726
payload.add(
@@ -810,10 +807,8 @@ void dfcc_instrumentt::instrument_assign(
810807
utils.make_null_check_expr(write_set), target_location));
811808

812809
payload.add(goto_programt::make_function_call(
813-
code_function_callt{
814-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEALLOCATED]
815-
.symbol_expr(),
816-
{write_set, dead_ptr.value()}},
810+
library.write_set_record_dead_call(
811+
write_set, dead_ptr.value(), target_location),
817812
target_location));
818813

819814
auto label_instruction =
@@ -846,10 +841,7 @@ void dfcc_instrumentt::instrument_assign(
846841
utils.make_null_check_expr(write_set), target_location));
847842

848843
payload.add(goto_programt::make_function_call(
849-
code_function_callt{
850-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_ALLOCATED]
851-
.symbol_expr(),
852-
{write_set, lhs}},
844+
library.write_set_add_allocated_call(write_set, lhs, target_location),
853845
target_location));
854846

855847
auto label_instruction =
@@ -987,11 +979,8 @@ void dfcc_instrumentt::instrument_deallocate_call(
987979
const auto &ptr = target->call_arguments().at(0);
988980

989981
payload.add(goto_programt::make_function_call(
990-
code_function_callt{
991-
check_var,
992-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_DEALLOCATE]
993-
.symbol_expr(),
994-
{write_set, ptr}},
982+
library.write_set_check_deallocate_call(
983+
check_var, write_set, ptr, target_location),
995984
target_location));
996985

997986
// add property class on assertion source_location
@@ -1005,10 +994,7 @@ void dfcc_instrumentt::instrument_deallocate_call(
1005994
payload.add(goto_programt::make_dead(check_var, target_location));
1006995

1007996
payload.add(goto_programt::make_function_call(
1008-
code_function_callt{
1009-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEALLOCATED]
1010-
.symbol_expr(),
1011-
{write_set, ptr}},
997+
library.write_set_record_deallocated_call(write_set, ptr, target_location),
1012998
target_location));
1013999

10141000
auto label_instruction =
@@ -1099,13 +1085,11 @@ void dfcc_instrumentt::instrument_other(
10991085

11001086
const auto &dest = target->get_other().operands().at(0);
11011087

1102-
symbolt &check_fun =
1103-
library.dfcc_fun_symbol
1104-
[is_array_set ? dfcc_funt::WRITE_SET_CHECK_ARRAY_SET
1105-
: dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY];
11061088
payload.add(goto_programt::make_function_call(
1107-
code_function_callt{
1108-
check_var, check_fun.symbol_expr(), {write_set, dest}},
1089+
is_array_set ? library.write_set_check_array_set_call(
1090+
check_var, write_set, dest, target_location)
1091+
: library.write_set_check_array_copy_call(
1092+
check_var, write_set, dest, target_location),
11091093
target_location));
11101094

11111095
// add property class on assertion source_location
@@ -1162,11 +1146,8 @@ void dfcc_instrumentt::instrument_other(
11621146
const auto &src = target->get_other().operands().at(1);
11631147

11641148
payload.add(goto_programt::make_function_call(
1165-
code_function_callt{
1166-
check_var,
1167-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE]
1168-
.symbol_expr(),
1169-
{write_set, dest, src}},
1149+
library.write_set_check_array_replace_call(
1150+
check_var, write_set, dest, src, target_location),
11701151
target_location));
11711152

11721153
// add property class on assertion source_location
@@ -1217,11 +1198,8 @@ void dfcc_instrumentt::instrument_other(
12171198
const auto &ptr = target->get_other().operands().at(0);
12181199

12191200
payload.add(goto_programt::make_function_call(
1220-
code_function_callt{
1221-
check_var,
1222-
library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT]
1223-
.symbol_expr(),
1224-
{write_set, ptr}},
1201+
library.write_set_check_havoc_object_call(
1202+
check_var, write_set, ptr, target_location),
12251203
target_location));
12261204

12271205
// add property class on assertion source_location

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

+4-6
Original file line numberDiff line numberDiff line change
@@ -60,12 +60,10 @@ void dfcc_is_freeablet::rewrite_calls(
6060
{
6161
// insert call to precondition for vacuity checking
6262
auto inst = goto_programt::make_function_call(
63-
code_function_callt{
64-
library
65-
.dfcc_fun_symbol
66-
[dfcc_funt::REPLACE_ENSURES_WAS_FREED_PRECONDITIONS]
67-
.symbol_expr(),
68-
{target->call_arguments().at(0), write_set}},
63+
library.check_replace_ensures_was_freed_preconditions_call(
64+
target->call_arguments().at(0),
65+
write_set,
66+
target->source_location()),
6967
target->source_location());
7068
program.insert_before_swap(target, inst);
7169
target++;

0 commit comments

Comments
 (0)