diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 17:43:16 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 17:43:16 +0200 |
| commit | f4b802ecd426fe594009817fde6df2dde8e08df2 (patch) | |
| tree | f38182626e714dd334fe7dd04b7d70ac4960b9ce /mppa_k1c/Asmblock.v | |
| parent | 6b191b047a12858230fe4976eae8a05e25b73a9a (diff) | |
| parent | 2e54a0fe8111e473361f9c1ab44b5d1cf9d70020 (diff) | |
| download | compcert-kvx-f4b802ecd426fe594009817fde6df2dde8e08df2.tar.gz compcert-kvx-f4b802ecd426fe594009817fde6df2dde8e08df2.zip | |
Merge remote-tracking branch 'origin/mppa_k1c' into mppa-work
Conflicts:
mppa_k1c/Asmblockdeps.v
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 408b8c31..e612576f 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1650,6 +1650,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. @@ -1709,6 +1711,7 @@ Ltac Equalities := - (* final states *) inv H; inv H0. congruence. Qed. +*) Definition data_preg (r: preg) : bool := match r with @@ -1721,7 +1724,7 @@ Definition data_preg (r: preg) : bool := (** Determinacy of the [Asm] semantics. *) -(* TODO. +(* Useless. Remark extcall_arguments_determ: forall rs m sg args1 args2, |