diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-12-06 21:34:46 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-12-06 21:34:46 +0100 |
| commit | 820e1ecbca864982ebc7b8efc453d057e374a4f7 (patch) | |
| tree | 260d27374b776f025c62a44f0ba08dcf4ea7a32f /scheduling | |
| parent | 47cdb65b2290df66690d34d6a09745fb364ef392 (diff) | |
| download | compcert-kvx-820e1ecbca864982ebc7b8efc453d057e374a4f7.tar.gz compcert-kvx-820e1ecbca864982ebc7b8efc453d057e374a4f7.zip | |
[Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6
starting a new index-verimag.html on BTL doc
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 52 |
1 files changed, 26 insertions, 26 deletions
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 55afc19a..b0765f09 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -122,9 +122,9 @@ with eval_smem ctx (sm: smem): option mem := (** The symbolic memory preserves predicate Mem.valid_pointer with respect to initial memory. Hence, arithmetic operations and Boolean conditions do not depend on the current memory of the block - (their semantics only depends on the initial memory of the block). + (their semantics only depends on the initial memory of the block). - The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. + The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. *) Lemma valid_pointer_preserv ctx sm: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs. @@ -308,31 +308,31 @@ Proof. Qed. Lemma eval_builtin_sval_arg ctx bs: - forall ba m v, - eval_builtin_sval ctx bs = Some ba -> - eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> - eval_builtin_sarg ctx m bs v. + forall ba m v, + eval_builtin_sval ctx bs = Some ba -> + eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> + eval_builtin_sarg ctx m bs v. Proof. - induction bs; simpl; - try (intros ba m v H; inversion H; subst; clear H; - intros H; inversion H; subst; - econstructor; auto; fail). - - intros ba m v; destruct (eval_sval _ _) eqn: SV; - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; auto. - - intros ba m v. - destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; eauto. - - intros ba m v. - destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; eauto. + induction bs; simpl; + try (intros ba m v H; inversion H; subst; clear H; + intros H; inversion H; subst; + econstructor; auto; fail). + - intros ba m v; destruct (eval_sval _ _) eqn: SV; + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; auto. + - intros ba m v. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. + - intros ba m v. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. Qed. Lemma eval_builtin_sarg_sval ctx m v: forall bs, |