Skip to content

Commit

Permalink
Make minor modifications
Browse files Browse the repository at this point in the history
  • Loading branch information
sonmarcho committed Nov 14, 2024
1 parent 5fc4491 commit 67f5498
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/llbc/Assumed.ml
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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<T>) -> &'a mut T {
Expand Down

0 comments on commit 67f5498

Please sign in to comment.