diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 08:59:28 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 08:59:28 +0100 |
| commit | 36f336d8c57f053342ec794e5bc802ebb66fc82b (patch) | |
| tree | a7ebad5e21735beb70ab1c36c63faa1e3a972024 /backend/ForwardMovesproof.v | |
| parent | 2e613cd29123583fb3378d5727217c359e818611 (diff) | |
| download | compcert-kvx-36f336d8c57f053342ec794e5bc802ebb66fc82b.tar.gz compcert-kvx-36f336d8c57f053342ec794e5bc802ebb66fc82b.zip | |
proof for jumptable
Diffstat (limited to 'backend/ForwardMovesproof.v')
| -rw-r--r-- | backend/ForwardMovesproof.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 6562fc7b..7727bc38 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -436,7 +436,23 @@ Proof. rewrite subst_arg_ok; eassumption. constructor; auto. - admit. + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. + apply list_nth_z_in with (n := Int.unsigned n). + assumption. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. (* return *) - destruct or as [arg | ]. |