From dd27d82c0c59ed99f47ec54b1ce8b34d2048bc3e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 7 Feb 2020 15:43:45 +0100
Subject: [PATCH] [Eva] Eval_terms: comments the function
 [contains_invalid_loc].

---
 src/plugins/value/legacy/eval_terms.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 370396757e4..13ffb2300d3 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)
-- 
GitLab