diff options
Diffstat (limited to 'src/Assumed.ml')
-rw-r--r-- | src/Assumed.ml | 69 |
1 files changed, 43 insertions, 26 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml index 5a9fb51b..527b2395 100644 --- a/src/Assumed.ml +++ b/src/Assumed.ml @@ -227,37 +227,54 @@ module Sig = struct let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true end -(** The list of assumed functions, and their signatures. +type assumed_info = A.assumed_fun_id * A.fun_sig * bool * Identifiers.name + +(** The list of assumed functions and all their information: + - their signature + - a boolean indicating whether they are monadic or not (i.e., if they + can fail or not) + - their name Rk.: following what is written above, we don't include `Box::free`. + + Remark about the vector functions: for `Vec::len` to be correct and return + a `usize`, we have to make sure that vectors are bounded by the max usize. + Followingly, `Vec::push` is monadic. *) -let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list = +let assumed_infos : assumed_info list = + let deref_pre = [ "core"; "ops"; "deref" ] in + let vec_pre = [ "alloc"; "vec"; "Vec" ] in + let index_pre = [ "core"; "ops"; "index" ] in [ - (Replace, Sig.mem_replace_sig); - (BoxNew, Sig.box_new_sig); - (BoxDeref, Sig.box_deref_shared_sig); - (BoxDerefMut, Sig.box_deref_mut_sig); - (VecNew, Sig.vec_new_sig); - (VecPush, Sig.vec_push_sig); - (VecInsert, Sig.vec_insert_sig); - (VecLen, Sig.vec_len_sig); - (VecIndex, Sig.vec_index_shared_sig); - (VecIndexMut, Sig.vec_index_mut_sig); + (Replace, Sig.mem_replace_sig, false, [ "core"; "mem"; "replace" ]); + (BoxNew, Sig.box_new_sig, false, [ "alloc"; "boxed"; "Box"; "new" ]); + (BoxDeref, Sig.box_deref_shared_sig, false, deref_pre @ [ "Deref"; "deref" ]); + ( BoxDerefMut, + Sig.box_deref_mut_sig, + false, + deref_pre @ [ "DerefMut"; "deref_mut" ] ); + (VecNew, Sig.vec_new_sig, false, vec_pre @ [ "new" ]); + (VecPush, Sig.vec_push_sig, true, vec_pre @ [ "push" ]); + (VecInsert, Sig.vec_insert_sig, true, vec_pre @ [ "insert" ]); + (VecLen, Sig.vec_len_sig, false, vec_pre @ [ "len" ]); + (VecIndex, Sig.vec_index_shared_sig, true, index_pre @ [ "Index"; "index" ]); + ( VecIndexMut, + Sig.vec_index_mut_sig, + true, + index_pre @ [ "IndexMut"; "index_mut" ] ); ] +let get_assumed_info (id : A.assumed_fun_id) : assumed_info = + List.find (fun (id', _, _, _) -> id = id') assumed_infos + let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig = - snd (List.find (fun (id', _) -> id = id') assumed_sigs) + let _, sg, _, _ = get_assumed_info id in + sg -let assumed_names : (A.assumed_fun_id * Identifiers.name) list = - [ - (Replace, [ "core"; "mem"; "replace" ]); - (BoxNew, [ "alloc"; "boxed"; "Box"; "new" ]); - (BoxDeref, [ "core"; "ops"; "deref"; "Deref"; "deref" ]); - (BoxDerefMut, [ "core"; "ops"; "deref"; "DerefMut"; "deref_mut" ]); - (VecNew, [ "alloc"; "vec"; "Vec"; "new" ]); - (VecPush, [ "alloc"; "vec"; "Vec"; "push" ]); - (VecInsert, [ "alloc"; "vec"; "Vec"; "insert" ]); - (VecLen, [ "alloc"; "vec"; "Vec"; "len" ]); - (VecIndex, [ "core"; "ops"; "index"; "Index"; "index" ]); - (VecIndexMut, [ "core"; "ops"; "index"; "IndexMut"; "index_mut" ]); - ] +let get_assumed_name (id : A.assumed_fun_id) : Identifiers.name = + let _, _, _, name = get_assumed_info id in + name + +let assumed_is_monadic (id : A.assumed_fun_id) : bool = + let _, _, b, _ = get_assumed_info id in + b |