diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-08-29 16:50:23 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:31 +0200 |
| commit | 63737a502b0f0b6c1369641e9d3d9f05712e74f7 (patch) | |
| tree | 920304519a0d4d20a519d4a810e9a3c2aae7ee05 /mppa_k1c/Asmblock.v | |
| parent | e2c15a3957cfcbab1ff0aaf30a8450c3e177a30a (diff) | |
| download | compcert-kvx-63737a502b0f0b6c1369641e9d3d9f05712e74f7.tar.gz compcert-kvx-63737a502b0f0b6c1369641e9d3d9f05712e74f7.zip | |
Asmblock: Adding forward_simulation and determinism as axioms
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 5c37021d..c83867f1 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1174,6 +1174,8 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +Axiom semantics_determinate: forall p, determinate (semantics p). + (** Determinacy of the [Asm] semantics. *) (* TODO. |