diff options
| author | Son Ho | 2022-02-08 18:37:46 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-08 18:37:46 +0100 |
| commit | 7e153990e307b2d83c00a333a91882317f9b16fc (patch) | |
| tree | 5419c90c2df67e55e3a7bcb64a310801bd39fda1 | |
| parent | 464e2da5f51547e4350871431f1e9ad74c48094f (diff) | |
Make minor modifications
Diffstat (limited to '')
| -rw-r--r-- | src/CfimAst.ml | 4 | ||||
| -rw-r--r-- | src/TranslateCore.ml | 6 |
2 files changed, 8 insertions, 2 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 2f8d3e69..a06dfc90 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -19,9 +19,9 @@ type var = { type assumed_fun_id = | Replace (** `core::mem::replace` *) | BoxNew - | BoxDeref (** `core::ops::deref::Deref::<alloc::boxed::Box::>::deref` *) + | BoxDeref (** `core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref` *) | BoxDerefMut - (** `core::ops::deref::DerefMut::<alloc::boxed::Box::>::deref_mut` *) + (** `core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut` *) | BoxFree | VecNew | VecPush diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 9dcbee02..e1a24e10 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -20,6 +20,12 @@ let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string = let fmt = PrintPure.mk_type_formatter type_defs type_params in PrintPure.type_def_to_string fmt def +let type_id_to_string (ctx : trans_ctx) (def : Pure.type_def) : string = + let type_params = def.type_params in + let type_defs = ctx.type_context.type_defs in + let fmt = PrintPure.mk_type_formatter type_defs type_params in + PrintPure.type_def_to_string fmt def + let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = let type_params = sg.type_params in let type_defs = ctx.type_context.type_defs in |