PR feedback

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

src/crab_verifier.hpp

@@ -35,11 +35,18 @@ void ebpf_verifier_clear_thread_local_state();
  * These constraints represent the program state at a specific point in the control flow graph,
  * as determined by the static analysis performed by the verifier.
  *
+ * If the 'store_pre_invariants' option is not set, this function will always return false along with an error message.
+ * This is because the verifier did not store the abstract constraints at each label.
+ *
+ * For invalid labels, this function will return false along with an error message.
+ *
  * @param[in,out] os Print output to this stream.
  * @param[in] label The location in the CFG to check against.
  * @param[in] constraints The concrete state to check.
  * @return true If the state is valid.
  * @return false If the state is invalid.
+ * @throw std::invalid_argument If the label format is invalid
+ * @throw std::out_of_range If the label value causes numeric overflow
  */
 bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label,
                                      const std::set<std::string>& constraints);
@@ -50,5 +57,7 @@ bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label,
  * @return The set of invariants at the given label.
  *         Each invariant represents a constraint on the program state at this point.
  *         Returns an empty set if no invariants are available.
+ * @throw std::invalid_argument If the label format is invalid
+ * @throw std::out_of_range If the label value causes numeric overflow
  */
-std::set<std::string> ebpf_get_invariants_at_label(const std::string& label);
+std::set<std::string> ebpf_get_invariants_at_label(const std::string& label);