Skip to content

Commit 4472173

Browse files
committed
Renamed contract application functions
The `code_contracts` function was unused and the function contract application part of it was improved in `replace_calls`. This commit: - removes this old unused functionality, - renames `code_contracts` to `apply_loop_contract`, and - renames `apply_contract` to `apply_function_contract`.
1 parent 7f998c4 commit 4472173

File tree

2 files changed

+7
-11
lines changed

2 files changed

+7
-11
lines changed

src/goto-instrument/code_contracts.cpp

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,7 @@ bool code_contractst::has_contract(const irep_idt fun_name)
158158
type.find(ID_C_spec_ensures).is_not_nil();
159159
}
160160

161-
bool code_contractst::apply_contract(
161+
bool code_contractst::apply_function_contract(
162162
goto_programt &goto_program,
163163
goto_programt::targett target)
164164
{
@@ -299,7 +299,7 @@ bool code_contractst::apply_contract(
299299
return false;
300300
}
301301

302-
void code_contractst::code_contracts(
302+
void code_contractst::apply_loop_contract(
303303
goto_functionst::goto_functiont &goto_function)
304304
{
305305
local_may_aliast local_may_alias(goto_function);
@@ -312,11 +312,6 @@ void code_contractst::code_contracts(
312312
l_it++)
313313
check_apply_invariants(
314314
goto_function, local_may_alias, l_it->first, l_it->second);
315-
316-
// look at all function calls
317-
Forall_goto_program_instructions(ins, goto_function.body)
318-
if(ins->is_function_call())
319-
apply_contract(goto_function.body, ins);
320315
}
321316

322317
const symbolt &code_contractst::new_tmp_symbol(
@@ -910,7 +905,7 @@ bool code_contractst::replace_calls(
910905
if(found == funs_to_replace.end())
911906
continue;
912907

913-
fail |= apply_contract(goto_function.second.body, ins);
908+
fail |= apply_function_contract(goto_function.second.body, ins);
914909
}
915910
}
916911
}

src/goto-instrument/code_contracts.h

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -133,13 +133,14 @@ class code_contractst
133133
goto_programt &created_decls,
134134
std::vector<exprt> &created_references);
135135

136-
void code_contracts(goto_functionst::goto_functiont &goto_function);
136+
void apply_loop_contract(goto_functionst::goto_functiont &goto_function);
137137

138138
/// \brief Does the named function have a contract?
139139
bool has_contract(const irep_idt);
140140

141-
bool
142-
apply_contract(goto_programt &goto_program, goto_programt::targett target);
141+
bool apply_function_contract(
142+
goto_programt &goto_program,
143+
goto_programt::targett target);
143144

144145
void
145146
add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);

0 commit comments

Comments
 (0)