mirror of
https://github.com/morluto/rea.git
synced 2026-11-14 10:43:30 +00:00
A terminal call on one branch does not end the whole function: other branches can still reach the following code, which stays in the body and pseudocode. The function-level limitation now says Ghidra excluded that call's fall-through and that code reachable only through it is missing if the callee returns. It is listed before the call-specific facts so a bounded composed summary that admits limitations in order keeps it. The body-coverage tests now check the counted records and their reasons instead of freezing the explanatory sentence. Co-Authored-By: gensokyo-dev <gensokyo-dev@users.noreply.github.com> Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>