diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml index 370396757e451c66c916f4c35aadec6cfede269e..13ffb2300d361dc1c7c9e14434997e9e78116197 100644 --- a/src/plugins/value/legacy/eval_terms.ml +++ b/src/plugins/value/legacy/eval_terms.ml @@ -133,6 +133,8 @@ let find_or_alarm ~alarm_mode state loc = track_alarms is_indeterminate alarm_mode; V_Or_Uninitialized.get_v v +(* Returns true if [loc] contains a memory location definitely invalid + for a memory access of kind [access]. *) let contains_invalid_loc access loc = let valid_loc = Locations.valid_part access loc in not (Locations.Location.equal loc valid_loc)