diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 16:47:18 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 16:47:18 +0100 |
| commit | 685c2f76b5f8b320495868cfdcadbf203f50a0bd (patch) | |
| tree | de1e379c6c99cdc94ecaf930318c79718dcce9cb /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 41109bd86942b028240ac20758ff29853b025534 (diff) | |
| download | compcert-kvx-685c2f76b5f8b320495868cfdcadbf203f50a0bd.tar.gz compcert-kvx-685c2f76b5f8b320495868cfdcadbf203f50a0bd.zip | |
Added Ointofsingle + floatconv unit test
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index ceea8de5..492687cd 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -154,7 +154,7 @@ Proof. 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.
+ all: try (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).
|