diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 12:00:16 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 12:00:16 +0100 |
| commit | 6462da4e8f25ce5df951635828901ad0180e9958 (patch) | |
| tree | ef5d83e00bd04f448ef46480bb5cd218175c6430 /mppa_k1c/Asmvliw.v | |
| parent | 92188c18a3761fa14dfdb97010cebe919548a010 (diff) | |
| download | compcert-kvx-6462da4e8f25ce5df951635828901ad0180e9958.tar.gz compcert-kvx-6462da4e8f25ce5df951635828901ad0180e9958.zip | |
Integrating Asmvliw.v in the proof chain
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 5b58118b..36c68acd 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -31,7 +31,8 @@ Require Import Locations. Require Stacklayout. Require Import Conventions. Require Import Errors. -Require Import Asmblock. +Require Export Asmblock. +Require Import Sorting.Permutation. Local Open Scope asm. @@ -236,8 +237,6 @@ Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m. -Require Import Sorting.Permutation. - Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop := exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with |