From 27d53418eff4e246a842a46b0883edda6860e3c2 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 1 Apr 2019 13:07:02 +0200 Subject: cleaning Asmvliw semantics --- mppa_k1c/Asmblock.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Asmblock.v') 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, -- cgit