From 3c5a3502623df93864e74b8d6819029fd7c68dd1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 27 Jan 2021 17:02:24 +0000 Subject: Finish all proofs except executing basic blocks --- src/hls/RTLPargenproof.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/hls/RTLPargenproof.v') diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 730ac98..0ff2312 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -171,4 +171,7 @@ Section CORRECTNESS. { destruct bb'; simplify; subst; repeat econstructor; eauto. } { destruct bb'; simplify; subst; repeat econstructor; eauto. } { destruct bb'; simplify; subst; repeat econstructor; eauto. } - { repeat econstructor; eauto. } + { unfold bind in *. destruct_match; try discriminate. repeat t. inv TRANSL0. + repeat econstructor; eauto. } + { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } + { inv STACKS. inv H1. repeat econstructor; eauto. } -- cgit