diff options
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, |