diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 16:24:56 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 16:24:56 +0100 |
| commit | 41109bd86942b028240ac20758ff29853b025534 (patch) | |
| tree | 71e37e2c7a2733da4e637d4242bd4d54964673fc /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 0a56ab26bc776468e6cf462cb5136fd62d4eb44a (diff) | |
| download | compcert-kvx-41109bd86942b028240ac20758ff29853b025534.tar.gz compcert-kvx-41109bd86942b028240ac20758ff29853b025534.zip | |
Added Osingleofint
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index d0aa89a4..ceea8de5 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -149,9 +149,12 @@ Lemma exec_basic_instr_pc_var: exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
Proof.
intros. unfold exec_basic_instr in *. destruct i.
- - unfold exec_arith_instr in *. exploreInst.
- all: try (inv H; apply next_eq; auto;
+ - unfold exec_arith_instr in *. destruct i; destruct i.
+ all: try (exploreInst; inv H; apply next_eq; auto;
apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
+
+ (* Some cases treated seperately because exploreInst destructs too much *)
+ inv H. apply next_eq; auto. apply functional_extensionality; intros. rewrite regset_double_set; auto. discriminate.
- exploreInst; apply exec_load_pc_var; auto.
- exploreInst; apply exec_store_pc_var; auto.
- destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
|