diff options
-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. |