diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 17:03:24 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 17:03:24 +0200 |
| commit | ee6b5b9e5445f64b26776cf16c2b9cef60b84574 (patch) | |
| tree | 190f5004b54074a8cc88fd9b16fb46292e410e44 /backend/Injectproof.v | |
| parent | 501d6501b9de645843cfa1e1408ba3fe9318223f (diff) | |
| download | compcert-kvx-ee6b5b9e5445f64b26776cf16c2b9cef60b84574.tar.gz compcert-kvx-ee6b5b9e5445f64b26776cf16c2b9cef60b84574.zip | |
internal call
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 12 |
1 files changed, 11 insertions, 1 deletions
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. |