From 3cf1d87a9bbfb7a1e29d4e3f919d3cd4ec3999c2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 16:27:57 +0100
Subject: Add a comment in Assumed.ml

---
 src/Assumed.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Assumed.ml b/src/Assumed.ml
index 52e52b10..2fc8dd61 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -1,5 +1,12 @@
 module T = Types
-(** This module contains various utilities for the assumed functions *)
+(** This module contains various utilities for the assumed functions.
+
+    Note that `Box::free` is peculiar: we don't really handle it as a function,
+    because it is legal to free a box whose boxed value is `⊥` (it often
+    happens that we move a value out of a box before freeing this box).
+    Semantically speaking, we thus handle `Box::free` as a value drop and
+    not as a function call, and thus never need its signature.
+ *)
 
 module A = CfimAst
 open TypesUtils
-- 
cgit v1.2.3