From a39b85fe1baa48e47261199971641bd71a5f0b0e Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Tue, 18 May 2021 11:49:20 +0100 Subject: Get Ireturn proof to pass again --- src/hls/HTLgenproof.v | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'src/hls/HTLgenproof.v') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 78b169f..db564af 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1328,14 +1328,13 @@ Section CORRECTNESS. + eapply HTL.step_finish; big_tac. + eauto with htlproof. - constructor; eauto with htlproof. - + edestruct empty_stack_free with (blk:=stk). eauto. - * enough (m' = m). - { subst. eauto. } - apply option_inv. - congruence. - * inv MF. - constructor. - discriminate. + + edestruct no_stack_functions; eauto. + * replace (RTL.fn_stacksize f) in *. + replace m' with m by + (pose proof (mem_free_zero m ltac:(auto)); crush). + subst. + assumption. + * subst. inv MF. constructor. + destruct or. * rewrite fso. (* Return value is not fin *) { @@ -1350,9 +1349,7 @@ Section CORRECTNESS. by (eapply RTL.max_reg_function_use; eauto; crush). xomega. * simpl. eauto with htlproof. - + destruct or; simpl; crush. - eauto using no_pointer_return. - + + destruct or; simpl; eauto using no_pointer_return. Unshelve. try exact tt; eauto. Qed. Hint Resolve transl_ireturn_correct : htlproof. -- cgit