From 7c18e5fbe3dee48b6a7f38d19cbb19427e6722fd Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 31 Mar 2020 17:07:23 +0200
Subject: external call

---
 backend/Injectproof.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'backend/Injectproof.v')

diff --git a/backend/Injectproof.v b/backend/Injectproof.v
index 40c39b89..c9493baf 100644
--- a/backend/Injectproof.v
+++ b/backend/Injectproof.v
@@ -1624,7 +1624,14 @@ Section INJECTOR.
           constructor; auto.
           rewrite params_preserved with (f:=f)(tf:=x) by assumption.
           apply match_regs_refl.
-      - admit.
+      - (* external call *)
+        monadInv FUN.
+        econstructor; split.
+        + apply Smallstep.plus_one.
+          apply exec_function_external.
+          eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+        + constructor; auto.
+        
       - admit.
     Admitted.
 
-- 
cgit