diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-18 11:49:20 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-18 11:49:20 +0100 |
| commit | a39b85fe1baa48e47261199971641bd71a5f0b0e (patch) | |
| tree | af2c2ddb8a2d11d03e580a1574f1f7277caa2df1 /src/hls/HTLgenproof.v | |
| parent | 44ced90ba3d75f29a929c8af2fb01bc63dc402b9 (diff) | |
| download | vericert-a39b85fe1baa48e47261199971641bd71a5f0b0e.tar.gz vericert-a39b85fe1baa48e47261199971641bd71a5f0b0e.zip | |
Get Ireturn proof to pass again
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 19 |
1 files changed, 8 insertions, 11 deletions
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. |