@@ -896,16 +896,16 @@ void code_contractst::apply_loop_contract(
896
896
897
897
for (const auto &loop_head_and_content : natural_loops.loop_map)
898
898
{
899
- const auto &loop_content = loop_head_and_content.second ;
899
+ const auto &loop_body = loop_head_and_content.second ;
900
900
// Skip empty loops and self-looped node.
901
- if (loop_content .size () <= 1 )
901
+ if (loop_body .size () <= 1 )
902
902
continue ;
903
903
904
904
auto loop_head = loop_head_and_content.first ;
905
905
auto loop_end = loop_head;
906
906
907
907
// Find the last back edge to `loop_head`
908
- for (const auto &t : loop_content )
908
+ for (const auto &t : loop_body )
909
909
{
910
910
if (
911
911
t->is_goto () && t->get_target () == loop_head &&
@@ -920,15 +920,15 @@ void code_contractst::apply_loop_contract(
920
920
throw 0 ;
921
921
}
922
922
923
- // By definition the `loop_content ` is a set of instructions computed
923
+ // By definition the `loop_body ` is a set of instructions computed
924
924
// by `natural_loops` based on the CFG.
925
925
// Since we perform assigns clause instrumentation by sequentially
926
926
// traversing instructions from `loop_head` to `loop_end`,
927
- // here we ensure that all instructions in `loop_content ` belong within
927
+ // here we ensure that all instructions in `loop_body ` belong within
928
928
// the [loop_head, loop_end] target range.
929
929
930
- // Check 1. (i \in loop_content ) ==> loop_head <= i <= loop_end
931
- for (const auto &i : loop_content )
930
+ // Check 1. (i \in loop_body ) ==> loop_head <= i <= loop_end
931
+ for (const auto &i : loop_body )
932
932
{
933
933
if (
934
934
loop_head->location_number > i->location_number ||
@@ -946,8 +946,7 @@ void code_contractst::apply_loop_contract(
946
946
}
947
947
}
948
948
949
- if (!loop_head_ends
950
- .emplace (loop_head, std::make_pair (loop_end, loop_content))
949
+ if (!loop_head_ends.emplace (loop_head, std::make_pair (loop_end, loop_body))
951
950
.second )
952
951
UNREACHABLE;
953
952
}
0 commit comments