Check for unreachable exit

[Alan-Jowett]

This pull request includes changes to improve the handling of unreachable code detection and adds new test cases for various infinite loop scenarios. The most important changes include adding a check for unreachable exit points in crab_verifier.cpp and introducing multiple test cases in loop.yaml to validate the new functionality.

Improvements to unreachable code detection:

• src/crab_verifier.cpp: Added a check to handle cases where the exit is unreachable, updating the database with an appropriate message.

Addition of new test cases:

• test-data/loop.yaml: Added multiple test cases to cover different types of simple infinite loops, ensuring the new unreachable code detection functionality is thoroughly tested.

Summary by CodeRabbit

• New Features

  • Enhanced logic for determining maximum loop count from post-invariants, improving accuracy.
  • Added multiple new test cases for various loop constructs and their termination conditions.

• Bug Fixes

  • Improved assessment of loop count to better handle edge cases, including unreachable exit labels.