diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-27 17:02:24 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-27 17:02:24 +0000 |
| commit | 3c5a3502623df93864e74b8d6819029fd7c68dd1 (patch) | |
| tree | 9df19493806125272d5afe515fe91df916dae2ee | |
| parent | 9432515e5814e8614c8f2320a8ae6d268065c9ff (diff) | |
| download | vericert-kvx-3c5a3502623df93864e74b8d6819029fd7c68dd1.tar.gz vericert-kvx-3c5a3502623df93864e74b8d6819029fd7c68dd1.zip | |
Finish all proofs except executing basic blocks
| -rw-r--r-- | src/hls/RTLPargenproof.v | 5 |
1 files changed, 4 insertions, 1 deletions
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. } |