diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 87 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 6 | ||||
| -rw-r--r-- | cfrontend/Cminorgen.v | 2 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 16 | ||||
| -rw-r--r-- | cfrontend/Ctypes.v | 56 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 2 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 10 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 4 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 2 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 10 |
10 files changed, 121 insertions, 74 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 84e24640..a7ee353a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -132,12 +132,34 @@ let string_of_errmsg msg = (** ** The builtin environment *) +let ais_annot_functions = + if Configuration.elf_target then + [(* Ais Annotations, only available for ELF targets *) + "__builtin_ais_annot", + (TVoid [], + [TPtr(TInt(IChar, [AConst]), [])], + true);] + else + [] + let builtins_generic = { Builtins.typedefs = []; - Builtins.functions = [ + Builtins.functions = + ais_annot_functions + @[ + (* Integer arithmetic *) + "__builtin_bswap", + (TInt(IUInt, []), [TInt(IUInt, [])], false); + "__builtin_bswap32", + (TInt(IUInt, []), [TInt(IUInt, [])], false); + "__builtin_bswap16", + (TInt(IUShort, []), [TInt(IUShort, [])], false); (* Floating-point absolute value *) "__builtin_fabs", - (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* Float arithmetic *) + "__builtin_fsqrt", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], @@ -200,63 +222,63 @@ let builtins_generic = { [TPtr(TVoid [], []); TInt(IULong, [])], false); (* Helper functions for int64 arithmetic *) - "__i64_dtos", + "__compcert_i64_dtos", (TInt(ILongLong, []), [TFloat(FDouble, [])], false); - "__i64_dtou", + "__compcert_i64_dtou", (TInt(IULongLong, []), [TFloat(FDouble, [])], false); - "__i64_stod", + "__compcert_i64_stod", (TFloat(FDouble, []), [TInt(ILongLong, [])], false); - "__i64_utod", + "__compcert_i64_utod", (TFloat(FDouble, []), [TInt(IULongLong, [])], false); - "__i64_stof", + "__compcert_i64_stof", (TFloat(FFloat, []), [TInt(ILongLong, [])], false); - "__i64_utof", + "__compcert_i64_utof", (TFloat(FFloat, []), [TInt(IULongLong, [])], false); - "__i64_sdiv", + "__compcert_i64_sdiv", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(ILongLong, [])], false); - "__i64_udiv", + "__compcert_i64_udiv", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], false); - "__i64_smod", + "__compcert_i64_smod", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(ILongLong, [])], false); - "__i64_umod", + "__compcert_i64_umod", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], false); - "__i64_shl", + "__compcert_i64_shl", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(IInt, [])], false); - "__i64_shr", + "__compcert_i64_shr", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IInt, [])], false); - "__i64_sar", + "__compcert_i64_sar", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(IInt, [])], false); - "__i64_smulh", + "__compcert_i64_smulh", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(ILongLong, [])], false); - "__i64_umulh", + "__compcert_i64_umulh", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], false) @@ -818,7 +840,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - AST.EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), + AST.EF_annot(P.of_int 1,coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "argument 1 of '__builtin_annot' must be a string literal"; @@ -830,7 +852,32 @@ let rec convertExpr env e = | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(AST.EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), + Ebuiltin(AST.EF_annot_val(P.of_int 1,coqstring_of_camlstring txt, typ_of_type targ), + Tcons(targ, Tnil), convertExprList env [arg], + convertTyp env e.etyp) + | _ -> + error "argument 1 of '__builtin_annot_intval' must be a string literal"; + ezero + end + + | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target -> + begin match args with + | {edesc = C.EConst(CStr txt)} :: args1 -> + let targs1 = convertTypArgs env [] args1 in + Ebuiltin( + AST.EF_annot(P.of_int 2,coqstring_of_camlstring txt, typlist_of_typelist targs1), + targs1, convertExprList env args1, convertTyp env e.etyp) + | _ -> + error "argument 1 of '__builtin_ais_annot' must be a string literal"; + ezero + end + + | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot_intval"}}, args) when Configuration.elf_target -> + begin match args with + | [ {edesc = C.EConst(CStr txt)}; arg ] -> + let targ = convertTyp env + (Cutil.default_argument_conversion env arg.etyp) in + Ebuiltin(AST.EF_annot_val(P.of_int 2,coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> @@ -1130,7 +1177,7 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__i64_" +let re_runtime = Str.regexp "__compcert_i64_" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index e063dfc3..823d2542 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -513,8 +513,8 @@ Definition do_external (ef: external_function): | EF_malloc => do_ef_malloc | EF_free => do_ef_free | EF_memcpy sz al => do_ef_memcpy sz al - | EF_annot text targs => do_ef_annot text targs - | EF_annot_val text targ => do_ef_annot_val text targ + | EF_annot kind text targs => do_ef_annot text targs + | EF_annot_val kind text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge | EF_debug kind text targs => do_ef_debug kind text targs end. @@ -1770,7 +1770,7 @@ Lemma not_stuckred_imm_safe: Proof. intros. generalize (step_expr_sound a k m). intros [A B]. destruct (step_expr k a m) as [|[C rd] res] eqn:?. - specialize (B (refl_equal _)). destruct k. + specialize (B (eq_refl _)). destruct k. destruct a; simpl in B; try congruence. constructor. destruct a; simpl in B; try congruence. constructor. assert (NOTSTUCK: rd <> Stuckred). diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 5017fc8e..45c21f96 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -226,7 +226,7 @@ Definition assign_variable let (id, sz) := id_sz in let (cenv, stacksize) := cenv_stacksize in let ofs := align stacksize (block_alignment sz) in - (PTree.set id ofs cenv, ofs + Zmax 0 sz). + (PTree.set id ofs cenv, ofs + Z.max 0 sz). Definition assign_variables (cenv_stacksize: compilenv * Z) (vars: list (ident * Z)) : compilenv * Z := List.fold_left assign_variable vars cenv_stacksize. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a6d58f17..ffafc5d2 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -96,7 +96,7 @@ Proof. intros m1 FR1 FRL. transitivity (Mem.load chunk m1 b ofs). eapply IHfbl; eauto. intros. eapply H. eauto with coqlib. - eapply Mem.load_free; eauto. left. apply sym_not_equal. eapply H. auto with coqlib. + eapply Mem.load_free; eauto. left. apply not_eq_sym. eapply H. auto with coqlib. Qed. Lemma perm_freelist: @@ -775,7 +775,7 @@ Definition cenv_compat (cenv: compilenv) (vars: list (ident * Z)) (tsz: Z) : Pro PTree.get id cenv = Some ofs /\ Mem.inj_offset_aligned ofs sz /\ 0 <= ofs - /\ ofs + Zmax 0 sz <= tsz. + /\ ofs + Z.max 0 sz <= tsz. Definition cenv_separated (cenv: compilenv) (vars: list (ident * Z)) : Prop := forall id1 sz1 ofs1 id2 sz2 ofs2, @@ -901,7 +901,7 @@ Remark assign_variable_incr: Proof. simpl; intros. inv H. generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)). - assert (0 <= Zmax 0 sz). apply Zmax_bound_l. omega. + assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega. omega. Qed. @@ -914,7 +914,7 @@ Proof. Opaque assign_variable. destruct a as [id s]. simpl. intros. destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?. - apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto. + apply Z.le_trans with sz1. eapply assign_variable_incr; eauto. eauto. Transparent assign_variable. Qed. @@ -925,8 +925,8 @@ Proof. intros; red; intros. apply Zdivides_trans with (block_alignment sz). unfold align_chunk. unfold block_alignment. - generalize Zone_divide; intro. - generalize Zdivide_refl; intro. + generalize Z.divide_1_l; intro. + generalize Z.divide_refl; intro. assert (2 | 4). exists 2; auto. assert (2 | 8). exists 4; auto. assert (4 | 8). exists 2; auto. @@ -942,10 +942,10 @@ Qed. Remark inj_offset_aligned_block': forall stacksize sz, - Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Zmax 0 sz). + Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz). Proof. intros. - replace (block_alignment sz) with (block_alignment (Zmax 0 sz)). + replace (block_alignment sz) with (block_alignment (Z.max 0 sz)). apply inj_offset_aligned_block. rewrite Zmax_spec. destruct (zlt sz 0); auto. transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 8d6cdb24..036b768b 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -373,15 +373,15 @@ Lemma sizeof_alignof_compat: forall env t, naturally_aligned t -> (alignof env t | sizeof env t). Proof. induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. -- apply Zdivide_refl. -- destruct i; apply Zdivide_refl. +- apply Z.divide_refl. +- destruct i; apply Z.divide_refl. - exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity. -- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. -- apply Zdivide_refl. +- destruct f. apply Z.divide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. +- apply Z.divide_refl. - apply Z.divide_mul_l; auto. -- apply Zdivide_refl. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. +- apply Z.divide_refl. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. Qed. (** ** Size and alignment for composite definitions *) @@ -435,9 +435,9 @@ Lemma sizeof_struct_incr: Proof. induction m as [|[id t]]; simpl; intros. - omega. -- apply Zle_trans with (align cur (alignof env t)). +- apply Z.le_trans with (align cur (alignof env t)). apply align_le. apply alignof_pos. - apply Zle_trans with (align cur (alignof env t) + sizeof env t). + apply Z.le_trans with (align cur (alignof env t) + sizeof env t). generalize (sizeof_pos env t); omega. apply IHm. Qed. @@ -488,7 +488,7 @@ Proof. inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr. exploit IHfld; eauto. intros [A B]. split; auto. - eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)). + eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)). apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. Qed. @@ -627,7 +627,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z := Lemma alignof_blockcopy_1248: forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. Proof. - assert (X: forall co, let a := Zmin 8 (co_alignof co) in + assert (X: forall co, let a := Z.min 8 (co_alignof co) in a = 1 \/ a = 2 \/ a = 4 \/ a = 8). { intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. @@ -635,7 +635,7 @@ Proof. destruct n; auto. destruct n; auto. right; right; right. apply Z.min_l. - rewrite two_power_nat_two_p. rewrite ! inj_S. + rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ. change 8 with (two_p 3). apply two_p_monotone. omega. } induction ty; simpl. @@ -661,28 +661,28 @@ Lemma sizeof_alignof_blockcopy_compat: Proof. assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)). { - intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof. + intros. apply Z.divide_trans with (co_alignof co). 2: apply co_sizeof_alignof. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. apply Z.min_case. exists (two_p (Z.of_nat n)). change 8 with (two_p 3). rewrite <- two_p_is_exp by omega. - rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. - apply Zdivide_refl. + rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega. + apply Z.divide_refl. } induction ty; simpl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. apply Z.divide_mul_l. auto. - apply Zdivide_refl. - destruct (env!i). apply X. apply Zdivide_0. - destruct (env!i). apply X. apply Zdivide_0. + apply Z.divide_refl. + destruct (env!i). apply X. apply Z.divide_0_r. + destruct (env!i). apply X. apply Z.divide_0_r. Qed. (** Type ranks *) @@ -707,7 +707,7 @@ Fixpoint rank_type (ce: composite_env) (t: type) : nat := Fixpoint rank_members (ce: composite_env) (m: members) : nat := match m with | nil => 0%nat - | (id, t) :: m => Peano.max (rank_type ce t) (rank_members ce m) + | (id, t) :: m => Init.Nat.max (rank_type ce t) (rank_members ce m) end. (** ** C types and back-end types *) @@ -818,7 +818,7 @@ Program Definition composite_of_def co_sizeof_alignof := _ |} end. Next Obligation. - apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. + apply Z.le_ge. eapply Z.le_trans. eapply sizeof_composite_pos. apply align_le; apply alignof_composite_pos. Defined. Next Obligation. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 388b6544..77d6cfea 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -186,7 +186,7 @@ Fixpoint transl_init_rec (ce: composite_env) (ty: type) (i: initializer) | Init_single a, _ => do d <- transl_init_single ce ty a; OK (d :: k) | Init_array il, Tarray tyelt nelt _ => - transl_init_array ce tyelt il (Zmax 0 nelt) k + transl_init_array ce tyelt il (Z.max 0 nelt) k | Init_struct il, Tstruct id _ => do co <- lookup_composite ce id; match co_su co with diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 524bc631..272b929f 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -486,7 +486,7 @@ Inductive tr_init: type -> initializer -> list init_data -> Prop := transl_init_single ge ty a = OK d -> tr_init ty (Init_single a) (d :: nil) | tr_init_arr: forall tyelt nelt attr il d, - tr_init_array tyelt il (Zmax 0 nelt) d -> + tr_init_array tyelt il (Z.max 0 nelt) d -> tr_init (Tarray tyelt nelt attr) (Init_array il) d | tr_init_str: forall id attr il co d, lookup_composite ge id = OK co -> co_su co = Struct -> @@ -723,7 +723,7 @@ Local Opaque sizeof. + rewrite idlsize_app, padding_size. exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. - apply Zle_trans with (sizeof_union ge (co_members co)). + apply Z.le_trans with (sizeof_union ge (co_members co)). eapply union_field_size; eauto. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite H0. apply align_le. @@ -816,9 +816,9 @@ Lemma store_init_data_list_app: Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''. Proof. induction data1; simpl; intros. - inv H. rewrite Zplus_0_r in H0. auto. + inv H. rewrite Z.add_0_r in H0. auto. destruct (Genv.store_init_data ge m b ofs a); try discriminate. - rewrite Zplus_assoc in H0. eauto. + rewrite Z.add_assoc in H0. eauto. Qed. Remark store_init_data_list_padding: @@ -874,7 +874,7 @@ Local Opaque sizeof. eapply store_init_data_list_app. eauto. rewrite (tr_init_size _ _ _ H9). - rewrite <- Zplus_assoc. eapply H2. eauto. eauto. + rewrite <- Z.add_assoc. eapply H2. eauto. eauto. apply align_le. apply alignof_pos. Qed. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 6366906a..6e016cb3 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -253,10 +253,10 @@ let rec expr p (prec, e) = fprintf p "__builtin_memcpy_aligned@[<hov 1>(%ld,@ %ld,@ %a)@]" (camlint_of_coqint sz) (camlint_of_coqint al) exprlist (true, args) - | Ebuiltin(EF_annot(txt, _), _, args, _) -> + | Ebuiltin(EF_annot(_,txt, _), _, args, _) -> fprintf p "__builtin_annot@[<hov 1>(%S%a)@]" (camlstring_of_coqstring txt) exprlist (false, args) - | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> + | Ebuiltin(EF_annot_val(_,txt, _), _, args, _) -> fprintf p "__builtin_annot_intval@[<hov 1>(%S%a)@]" (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_external(id, sg), _, args, _) -> diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 0a191f29..45b686f3 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -80,7 +80,7 @@ Definition initial_generator (x: unit) : generator := Definition gensym (ty: type): mon ident := fun (g: generator) => Res (gen_next g) - (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g)) + (mkgenerator (Pos.succ (gen_next g)) ((gen_next g, ty) :: gen_trail g)) (Ple_succ (gen_next g)). (** Construct a sequence from a list of statements. To facilitate the diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 8ed924e5..7af499f4 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -604,7 +604,7 @@ Proof. destruct (peq id id0). inv A. right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C. - subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ. + subst b. split. apply Ple_refl. eapply Pos.lt_le_trans; eauto. rewrite B. apply Plt_succ. auto. right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. Qed. @@ -696,7 +696,7 @@ Proof. (* variable is not lifted out of memory *) exploit Mem.alloc_parallel_inject. - eauto. eauto. apply Zle_refl. apply Zle_refl. + eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [j1 [tm1 [tb1 [A [B [C [D E]]]]]]]. exploit IHalloc_variables; eauto. instantiate (1 := PTree.set id (tb1, ty) te). intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]]. @@ -778,8 +778,8 @@ Proof. apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2. destruct (peq id0 id). inv H2. eapply Mem.load_alloc_same'; eauto. - omega. rewrite Zplus_0_l. eapply sizeof_by_value; eauto. - apply Zdivide_0. + omega. rewrite Z.add_0_l. eapply sizeof_by_value; eauto. + apply Z.divide_0_r. eapply Mem.load_alloc_other; eauto. Qed. @@ -1053,7 +1053,7 @@ Proof. assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). - replace (sizeof tge ty) with (Z_of_nat (length bytes)). + replace (sizeof tge ty) with (Z.of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). |