@@ -896,16 +896,16 @@ void code_contractst::apply_loop_contract(
896896
897897 for (const auto &loop_head_and_content : natural_loops.loop_map)
898898 {
899- const auto &loop_content = loop_head_and_content.second ;
899+ const auto &loop_body = loop_head_and_content.second ;
900900 // Skip empty loops and self-looped node.
901- if (loop_content .size () <= 1 )
901+ if (loop_body .size () <= 1 )
902902 continue ;
903903
904904 auto loop_head = loop_head_and_content.first ;
905905 auto loop_end = loop_head;
906906
907907 // Find the last back edge to `loop_head`
908- for (const auto &t : loop_content )
908+ for (const auto &t : loop_body )
909909 {
910910 if (
911911 t->is_goto () && t->get_target () == loop_head &&
@@ -920,15 +920,15 @@ void code_contractst::apply_loop_contract(
920920 throw 0 ;
921921 }
922922
923- // By definition the `loop_content ` is a set of instructions computed
923+ // By definition the `loop_body ` is a set of instructions computed
924924 // by `natural_loops` based on the CFG.
925925 // Since we perform assigns clause instrumentation by sequentially
926926 // 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
928928 // the [loop_head, loop_end] target range.
929929
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 )
932932 {
933933 if (
934934 loop_head->location_number > i->location_number ||
@@ -946,8 +946,7 @@ void code_contractst::apply_loop_contract(
946946 }
947947 }
948948
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))
951950 .second )
952951 UNREACHABLE;
953952 }
0 commit comments