From a26610bc11e2c74b8caac1f74979fc2d010d632c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 19:23:47 +0200 Subject: progress in proofs --- backend/Profilingproof.v | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'backend/Profilingproof.v') 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. -- cgit