PR feedback

Signed-off-by: Alan Jowett <[email protected]>

src/crab_verifier.hpp

@@ -46,8 +46,9 @@ bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label,
 /**
  * @brief Get the invariants at a given label. Requires the `store_pre_invariants` option to be set.
  *
- * @param[in] label
+ * @param[in] label The label in the CFG where invariants should be retrieved
  * @return The set of invariants at the given label.
+ *         Each invariant represents a constraint on the program state at this point.
  * @throw std::out_of_range If the label is not found.
  */
 std::set<std::string> ebpf_get_invariants_at_label(const std::string& label);

src/test/ebpf_yaml.cpp

@@ -290,7 +290,7 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
                 actual_messages.insert(label + ": Concrete invariants do not match abstract invariants");
             }
         } catch (const std::exception& e) {
-            actual_messages.insert(label + ": Exception occurred during invariant check - " + std::string(e.what()));
+            actual_messages.insert(label + ": Exception occurred during invariant check");
         }
     }
 

test-data/add.yaml

@@ -242,7 +242,8 @@ invariants-to-check:
     - r2.svalue=2
     - r2.uvalue=2
 
-  3: # After the addition, r1 should be 3. Invalid invariant to test negative case.
+  3: # After the addition, r1 should be 3.
+     # Using a value of 2 instead of 3 to ensure that the test fails (this is a negative test case).
     - r1.type=number
     - r1.svalue=2
     - r1.uvalue=2