diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-12-03 11:20:59 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-12-03 11:20:59 +0100 |
| commit | 13e381fae01360f25bd01cb95b470ead906748e1 (patch) | |
| tree | c6a80a45c79150ef37772ccce3e5a284f3a9cae2 /mppa_k1c/Asm.v | |
| parent | 79a2dac7e5317e515ce9610db1d48d0fc9ff0708 (diff) | |
| download | compcert-kvx-13e381fae01360f25bd01cb95b470ead906748e1.tar.gz compcert-kvx-13e381fae01360f25bd01cb95b470ead906748e1.zip | |
Introducing ;; as Pcomma in Asm.v
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 17cd67f4..520bc453 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -47,6 +47,7 @@ Inductive instruction : Type := | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
| Pbuiltin: external_function -> list (builtin_arg preg)
-> builtin_res preg -> instruction (**r built-in function (pseudo) *)
+ | Psemi (**r semi colon separating bundles *)
| Pnop (**r instruction that does nothing *)
(** builtins *)
@@ -280,7 +281,7 @@ Definition unfold_exit (oc: option control) := | Some c => control_to_instruction c :: nil
end.
-Definition unfold_bblock (b: bblock) := unfold_label (header b) ++ unfold_body (body b) ++ unfold_exit (exit b).
+Definition unfold_bblock (b: bblock) := unfold_label (header b) ++ unfold_body (body b) ++ unfold_exit (exit b) ++ Psemi :: nil.
Fixpoint unfold (lb: bblocks) :=
match lb with
|