diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:23:47 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 19:23:47 +0200 |
| commit | a26610bc11e2c74b8caac1f74979fc2d010d632c (patch) | |
| tree | d549f902d0a2ae2af79118d40c0a4d8d5aff7f62 /backend/Profilingproof.v | |
| parent | 44e48a67a58a171ca29f22e15429b1baaf64ae81 (diff) | |
| download | compcert-kvx-a26610bc11e2c74b8caac1f74979fc2d010d632c.tar.gz compcert-kvx-a26610bc11e2c74b8caac1f74979fc2d010d632c.zip | |
progress in proofs
Diffstat (limited to 'backend/Profilingproof.v')
| -rw-r--r-- | backend/Profilingproof.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index ed07443c..72023792 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -279,11 +279,16 @@ Proof. + apply plus_one. apply exec_Ireturn. erewrite transf_function_at; eauto. apply I. - rewrite stacksize_preserved. - eassumption. + rewrite stacksize_preserved. eassumption. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_function_internal. + rewrite stacksize_preserved. eassumption. + + constructor; auto. + - econstructor; split. + + apply plus_one. apply exec_function_external. + eauto with profiling. + constructor; auto. - - admit. - - admit. - inv STACKS. inv H1. econstructor; split. + apply plus_one. apply exec_return. |