cda: mark functions with loops as potentially non-returning

[vmihalko]

Problem

LLVMInterprocCD::computeFuncInfo() seeds the noret set (instructions
after which a function may not return) using two mechanisms:

1. Syntactic — blocks with no successors and no ReturnInst: catches
   unreachable / abort() / exit()
2. Callee propagation — if a callee's noret set is non-empty, mark the
   call site

Both miss functions that contain loops:

• Definite case: no ReturnInst is reachable but the back-edge prevents
  hasNoSuccessors. Example: while(1);
• Conditional case: the loop exit depends on a runtime/nondet value so a
  ReturnInst is reachable on one path, but the loop may spin forever.
  Example: while(__VERIFIER_nondet_int());

In both cases the slicer drops code that appears after a call to such a
function — the call is not treated as a potential noret point so no
interprocedural control dependency is created.

For the termination property this causes a false negative: the
instrumented __INSTR_fail assert is sliced away before KLEE can reach it.

Fix

Use LLVM LoopInfo to detect natural loops in the function.
Every loop header's terminator is added to info.noret.

This is a sound over-approximation — any function with a reachable loop
may not return. External/library functions (isDeclaration()) are
unaffected. The fix applies to all CD algorithms (NTSCD, SCD) since
LLVMInterprocCD is constructed unconditionally for all of them.

Known limitation

The fix is coarse: bounded loops such as for (i = 0; i < 10; i++) also mark
the function as potentially noret. A future refinement could use
ScalarEvolution::getSmallConstantTripCount() to skip provably bounded loops.

Testing

Unit tests — dg slicing suite

	With fix	Without fix
Passing	166 / 174	166 / 174
Failing (pre-existing)	8	8

No regressions. New regression test added:
tests/slicing/sources/interproc-loop-noret.c — verifies that code after a
call to a looping function survives slicing.

SV-COMP termination benchmarks

2621 tasks, 60 s time limit, NTSCD algorithm (symbiotic --sv-comp --prp=termination ...).

Verdict	With fix	Without fix
true	818	820
false(termination)	639	639
TIMEOUT	936	934
ERROR	228	228

The 2 verdict differences (true → TIMEOUT) are timing noise at the 60 s
boundary, not caused by this change.

Slice size impact (from sbt-slicer logs):

• 200 / 2508 tasks (8%) have larger slices with the fix — all from programs
  with loops inside called functions (Linux driver models, dietlibc string
  functions)