diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 2 | ||||
| -rw-r--r-- | src/type_internal.ml | 12 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 479ecdca..71688ff6 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -1137,6 +1137,8 @@ let clear_low_order_bits_of_address a = end end +val translate_address : string -> addres -> maybe address * maybe nat + val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) let byte_list_of_memory_value endian mv = let mv = if endian = E_big_endian then mv else List.reverse mv in diff --git a/src/type_internal.ml b/src/type_internal.ml index 625c5357..26b68fa6 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -3029,13 +3029,15 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [] (*[LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] (*This constraint failing should be a warning, but truncation is ok*)*) in - let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in + let tannot = (l, Base(([],t2), External (Some "to_vec_inc"), cs, + pure_e, (get_cummulative_effects (get_eannot e)), bounds)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [] (* See above [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in - let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in + let tannot = (l, Base(([],t2),External (Some "to_vec_dec"), + cs, pure_e, (get_cummulative_effects (get_eannot e)),bounds)) in (*let _ = Printf.eprintf "Generating to_vec_dec call: bounds are %s\n" (bounds_to_string bounds) in*) (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) @@ -3049,13 +3051,15 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in - let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in + let tannot = (l, Base(([],t2), External(Some "to_vec_inc"), cs, pure_e, + (get_cummulative_effects (get_eannot e)), bounds)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in - let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in + let tannot = (l, Base(([],t2), External (Some "to_vec_dec"), cs, pure_e, + (get_cummulative_effects (get_eannot e)), bounds)) in (*let _ = Printf.eprintf "Generating to_vec_dec call: bounds are %s\n" (bounds_to_string bounds) in*) (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) |