16 : log(message_handler)
26 "symex-complexity-failed-child-loops-limit");
34 if(failed_child_loops_limit > 0)
46 for(
auto frame_iter = current_call_stack.rbegin();
47 frame_iter != current_call_stack.rend();
52 if(!frame_iter->active_loops.empty())
54 return &frame_iter->active_loops.back();
65 for(
auto frame_iter = current_call_stack.rbegin();
66 frame_iter != current_call_stack.rend();
69 for(
auto &loop_iter : frame_iter->active_loops)
71 for(
auto &blacklisted_loop : loop_iter.blacklisted_loops)
73 if(blacklisted_loop.get().contains(instr))
87 std::size_t sum_complexity = 0;
102 for(
auto frame_iter = current_call_stack.rbegin();
103 frame_iter != current_call_stack.rend();
106 for(
auto it = frame_iter->active_loops.rbegin();
107 it != frame_iter->active_loops.rend();
110 auto &loop_info = *it;
115 if(loop_to_blacklist)
117 loop_info.blacklisted_loops.emplace_back(*loop_to_blacklist);
121 sum_complexity += loop_info.children_too_complex;
125 std::reference_wrapper<lexical_loopst::loopt>(loop_info.loop);
131 return !loop_to_blacklist;
144 auto ¤t_call_stack = state.
call_stack();
152 if(active_loop !=
nullptr)
154 active_loop->children_too_complex++;
160 <<
"[symex-complexity] Loop operations considered too complex"
161 << (state.
source.
pc->source_location.is_not_nil()
162 ?
" at: " + state.
source.
pc->source_location.as_string()
163 :
", location number: " +
171 log.
warning() <<
"[symex-complexity] Branch considered too complex"
172 << (state.
source.
pc->source_location.is_not_nil()
173 ?
" at: " + state.
source.
pc->source_location.as_string()
174 :
", location number: " +
191 log.
warning() <<
"[symex-complexity] Trying to enter blacklisted loop"
192 << (state.
source.
pc->source_location.is_not_nil()
193 ?
" at: " + state.
source.
pc->source_location.as_string()
194 :
", location number: " +
213 transform_lambda.transform(complexity_violation, current_state);