Resolves: #728

This pull request exposes a new API "ebpf_check_constraints_at_label" which permits the caller to compare a set of constraints against the model at a specific label. If the model and the constraints differ it will return the two sets of constraints.

Enhancements and New Features:

• src/asm_parse.hpp: Exposed existing function to parse linear constraints.
• src/asm_syntax.hpp: Extended the label_t struct to support initialization from a string label.
• src/config.hpp: Added a new option to store pre-invariants in the verifier options.
• src/crab_verifier.cpp: Implemented functions to store pre-invariants and check constraints at specific labels. [1] [2] [3] [4]
• src/crab_verifier.hpp: Declared the new function for checking constraints at a label.

Test Case Updates:

• src/ebpf_yaml.cpp: Updated YAML parsing to include invariants to check and modified test case execution to validate these invariants. [1] [2] [3] [4] [5]
• src/ebpf_yaml.hpp: Added a new field to the TestCase struct for invariants to check.
• test-data/add.yaml: Added a new test case to check concrete state invariants.

Summary by CodeRabbit

Release Notes

• New Features

  • Introduced a new constructor for label parsing capabilities in label_t.
  • Added a boolean option store_pre_invariants for managing pre-invariant states during verification.
  • Implemented functions to check constraints and retrieve invariants associated with specific labels.
  • Added a new function for parsing linear constraints from strings.
  • Enhanced the testing framework to validate invariants during test execution.

• Bug Fixes

  • Improved error handling for invalid label formats and numeric overflow in new functions.

• Tests

  • Added new test cases to validate concrete state and invariants.

• Documentation

  • Updated documentation for new functions, detailing parameters and return types.