From e38366c52fc76edbca3e2842375fdab017356427 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 19:14:02 +0200 Subject: progress in proofs --- backend/Profilingproof.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'backend/Profilingproof.v') diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index 202e451c..fd905a39 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -248,7 +248,12 @@ Proof. + constructor; auto. constructor; auto. constructor. - - admit. + - econstructor; split. + + apply plus_one. apply exec_Itailcall with (sig:=(funsig fd)) (ros:=ros). + erewrite transf_function_at; eauto. apply I. + apply find_function_translated with (fd := fd). + all: eauto with profiling. + + constructor; auto. - admit. - admit. - admit. -- cgit