diff options
Diffstat (limited to 'backend/Tunnelingproof.v')
| -rw-r--r-- | backend/Tunnelingproof.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 774ce853..9a14158f 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -308,6 +308,14 @@ Proof. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. + (* Lbuiltin *) + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. + left; econstructor; split. + eapply exec_Lbuiltin; eauto. + rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. (* cond *) generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. |