diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-01 13:07:02 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-01 13:07:02 +0200 |
| commit | 27d53418eff4e246a842a46b0883edda6860e3c2 (patch) | |
| tree | 2b285fb2d26e212f48e5dc954ac9ec6092dddab8 /mppa_k1c/Asmblock.v | |
| parent | 2cbb81b2679a6d2b25bf490528060b321117294c (diff) | |
| download | compcert-kvx-27d53418eff4e246a842a46b0883edda6860e3c2.tar.gz compcert-kvx-27d53418eff4e246a842a46b0883edda6860e3c2.zip | |
cleaning Asmvliw semantics
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b4cf57ae..f3f59f7d 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1636,6 +1636,8 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +(* Useless + Remark extcall_arguments_determ: forall rs m sg args1 args2, extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. @@ -1695,6 +1697,7 @@ Ltac Equalities := - (* final states *) inv H; inv H0. congruence. Qed. +*) Definition data_preg (r: preg) : bool := match r with @@ -1707,7 +1710,7 @@ Definition data_preg (r: preg) : bool := (** Determinacy of the [Asm] semantics. *) -(* TODO. +(* Useless. Remark extcall_arguments_determ: forall rs m sg args1 args2, |