diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-11 16:11:22 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-11 16:11:22 +0100 |
| commit | b66c1d482292c15e3d7907262cf1c94edabdd40e (patch) | |
| tree | f9f8040471ab1e32eacb57e29a86838e7f8f86ae /mppa_k1c/PostpassSchedulingproof.v | |
| parent | bc162e5d2be64ea3f552a61155211c2d6a1beb76 (diff) | |
| download | compcert-kvx-b66c1d482292c15e3d7907262cf1c94edabdd40e.tar.gz compcert-kvx-b66c1d482292c15e3d7907262cf1c94edabdd40e.zip | |
Proving verified_schedule_size axiom
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 756e9a9e..64489e16 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -56,11 +56,6 @@ Axiom verified_schedule_correct: concat_all lbb = OK tbb
/\ bblock_equiv ge f bb tbb.
-Axiom verified_schedule_size:
- forall bb lbb,
- verified_schedule bb = OK lbb ->
- size bb = size_blocks lbb.
-
Axiom verified_schedule_single_inst: forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).
Axiom verified_schedule_header:
|