From 67f5498ac56c1357a51bdb9278a1ff17ff14ee10 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 14 Nov 2024 18:43:08 +0100 Subject: [PATCH] Make minor modifications --- src/llbc/Assumed.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/llbc/Assumed.ml b/src/llbc/Assumed.ml index 5a721fbb..707c654f 100644 --- a/src/llbc/Assumed.ml +++ b/src/llbc/Assumed.ml @@ -1,4 +1,4 @@ -(** This module contains various utilities for the assumed functions. +(** This module contains various utilities for the builtin 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 @@ -7,10 +7,10 @@ not as a function call, and thus never need its signature. TODO: implementing the concrete evaluation functions for the - assumed functions is really annoying (see + builtin functions is really annoying (see [InterpreterStatements.eval_non_local_function_call_concrete]), I think it should be possible, in most situations, to write bodies which - model the behaviour of those unsafe functions. For instance, [Box::deref_mut] + model the behavior of those functions. For instance, [Box::deref_mut] should simply be: {[ fn deref_mut<'a, T>(x : &'a mut Box) -> &'a mut T {