Commit 39710f78 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Register X1 is destroyed by some built-in functions

E.g. __builtin_bswap.  Update Asm modeling of builtins accordingly.
parent 7b3bc191
......@@ -1080,7 +1080,7 @@ Inductive step: state -> trace -> state -> Prop :=
rs' = nextinstr
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef))
(rs#X31 <- Vundef))) ->
(rs #X1 <- Vundef #X31 <- Vundef))) ->
step (State rs m) t (State rs' m')
| exec_step_external:
forall b ef args res rs m t rs' m',
......
......@@ -835,13 +835,15 @@ Local Transparent destroyed_by_op.
econstructor; eauto.
instantiate (2 := tf); instantiate (1 := x).
unfold nextinstr. rewrite Pregmap.gss.
rewrite set_res_other. rewrite undef_regs_other_2. rewrite Pregmap.gso by congruence.
rewrite set_res_other. rewrite undef_regs_other_2.
rewrite ! Pregmap.gso by congruence.
rewrite <- H1. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
rewrite preg_notin_charact. intros. auto with asmgen.
auto with asmgen.
apply agree_nextinstr. eapply agree_set_res; auto.
eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. apply Pregmap.gso; auto with asmgen.
eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
rewrite ! Pregmap.gso; auto with asmgen.
congruence.
- (* Mgoto *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment