From ee6b5b9e5445f64b26776cf16c2b9cef60b84574 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 17:03:24 +0200 Subject: internal call --- backend/Injectproof.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 013bc247..40c39b89 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1613,7 +1613,17 @@ Section INJECTOR. constructor; auto. ** constructor; auto. - - admit. + - (* internal call *) + monadInv FUN. + econstructor; split. + + apply Smallstep.plus_one. + apply exec_function_internal. + rewrite stacksize_preserved with (f:=f) by assumption. + eassumption. + + rewrite entrypoint_preserved with (f:=f)(tf:=x) by assumption. + constructor; auto. + rewrite params_preserved with (f:=f)(tf:=x) by assumption. + apply match_regs_refl. - admit. - admit. Admitted. -- cgit