Add a comment in Assumed.ml

1 files changed, 8 insertions, 1 deletions

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