diff options
| author | Timothy Bourke <tim@tbrk.org> | 2019-04-20 19:27:50 +0200 |
|---|---|---|
| committer | Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> | 2020-04-21 01:08:58 +0200 |
| commit | f8da0614e106a324fa6646213db68f2045070af4 (patch) | |
| tree | 029bd533a0e611a2b3d1f7512fd49505e6793859 | |
| parent | a3cf22317821f9f32e632344d51834a9a1524701 (diff) | |
| download | compcert-kvx-f8da0614e106a324fa6646213db68f2045070af4.tar.gz compcert-kvx-f8da0614e106a324fa6646213db68f2045070af4.zip | |
Fix rebase of Stackingproof/elab_char_constant
| -rw-r--r-- | backend/Stackingproof.v | 8 | ||||
| -rw-r--r-- | common/Separation.v | 2 | ||||
| -rw-r--r-- | cparser/Elab.mli | 6 |
3 files changed, 6 insertions, 10 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 79ef016a..d8b81689 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -149,7 +149,7 @@ Lemma contains_get_stack: Proof. intros. unfold load_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). - eapply loadv_rule; eauto. + eapply loadv_rule; eauto using perm_F_any. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. @@ -171,7 +171,7 @@ Lemma contains_set_stack: Proof. intros. unfold store_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). - eapply storev_rule; eauto. + eapply storev_rule; eauto using perm_F_any. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. @@ -1087,14 +1087,14 @@ Local Opaque b fe. apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto. (* Store of parent *) rewrite sep_swap3 in SEP. - apply (range_contains Mptr) in SEP; [|tauto]. + apply range_contains in SEP;[|apply perm_F_any|tauto]. exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr). rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m3' & STORE_PARENT & SEP). rewrite sep_swap3 in SEP. (* Store of return address *) rewrite sep_swap4 in SEP. - apply (range_contains Mptr) in SEP; [|tauto]. + apply range_contains in SEP; [|apply perm_F_any|tauto]. exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tptr). rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m4' & STORE_RETADDR & SEP). diff --git a/common/Separation.v b/common/Separation.v index 0aebb3c7..2804fd73 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -29,7 +29,7 @@ frame rule; instead, a weak form of the frame rule is provided by the lemmas that help us reason about the logical assertions. *) -Require Import Setoid Program.Basics. +Require Import Setoid Morphisms Program.Basics. Require Import Coqlib Decidableplus. Require Import AST Integers Values Memory Events Globalenvs. diff --git a/cparser/Elab.mli b/cparser/Elab.mli index 31d9b281..68e33d06 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -13,10 +13,6 @@ (* *) (* *********************************************************************) -val elab_int_constant : Cabs.cabsloc -> string -> int64 * C.ikind -val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind -val elab_char_constant : Cabs.cabsloc -> bool -> int64 list -> int64 * C.ikind - val elab_file : Cabs.definition list -> C.program (* This is the main entry point. It transforms a list of toplevel definitions as produced by the parser into a program in C abstract @@ -24,6 +20,6 @@ val elab_file : Cabs.definition list -> C.program val elab_int_constant : Cabs.loc -> string -> int64 * C.ikind val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind -val elab_char_constant : Cabs.loc -> bool -> int64 list -> int64 +val elab_char_constant : Cabs.loc -> bool -> int64 list -> int64 * C.ikind (* These auxiliary functions are exported so that they can be reused in other projects that deal with C-style source languages. *) |