diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-06-26 14:09:33 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:30 +0200 |
| commit | 7dca5905e7921b72634c31ae8de1bd08b3ff2e2e (patch) | |
| tree | 965aebe90748c9bd3cd036e4d656aeb3bb4b0357 /mppa_k1c/Machblock.v | |
| parent | 0236781c3ff798b60c5c8171a0f9b6cd569f7995 (diff) | |
| download | compcert-kvx-7dca5905e7921b72634c31ae8de1bd08b3ff2e2e.tar.gz compcert-kvx-7dca5905e7921b72634c31ae8de1bd08b3ff2e2e.zip | |
Machblock: some cleaning
Diffstat (limited to 'mppa_k1c/Machblock.v')
| -rw-r--r-- | mppa_k1c/Machblock.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/mppa_k1c/Machblock.v b/mppa_k1c/Machblock.v index 9b36fc43..6d28844b 100644 --- a/mppa_k1c/Machblock.v +++ b/mppa_k1c/Machblock.v @@ -55,7 +55,7 @@ Proof. Qed. Definition length_opt {A} (o: option A) : nat := - match o with + match o with | Some o => 1 | None => 0 end. @@ -110,10 +110,11 @@ Qed. Local Open Scope nat_scope. +(* FIXME - avoir une définition un peu plus simple, au prix de la preuve Mach -> Machblock ? *) Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := match c with | nil => None - | bb1 :: bbl => if is_label lbl bb1 + | bb1 :: bbl => if is_label lbl bb1 then let bb' := {| header := None ; body := body bb1 ; exit := exit bb1 |} in ( Some (match size bb' with | O => bbl @@ -191,7 +192,7 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m: | exec_MBsetstack: forall src ofs ty m' rs', store_stack m sp ty ofs (rs src) = Some m' -> - rs' = undef_regs (destroyed_by_setstack ty) rs -> + rs' = undef_regs (destroyed_by_setstack ty) rs -> basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m' | exec_MBgetparam: forall ofs ty dst v rs' f, @@ -225,8 +226,8 @@ Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> re forall rs m, body_step s f sp nil rs m rs m | exec_cons_body: - forall rs m bi p rs' m' rs'' m'', - basic_step s f sp rs m bi rs' m' -> + forall rs m bi p rs' m' rs'' m'', + basic_step s f sp rs m bi rs' m' -> body_step s f sp p rs' m' rs'' m'' -> body_step s f sp (bi::p) rs m rs'' m'' . |