diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-23 11:54:11 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-23 11:54:11 +0000 |
| commit | ece46e22da61e8a8d40766c533bcf2dd760deccb (patch) | |
| tree | e1c1cb8fb9a2ecb13342e826644baf75b0d749b9 | |
| parent | d460696e02f02ae25752678652757da11a44f50a (diff) | |
| download | vericert-kvx-ece46e22da61e8a8d40766c533bcf2dd760deccb.tar.gz vericert-kvx-ece46e22da61e8a8d40766c533bcf2dd760deccb.zip | |
Remove match on basic blocks
| -rw-r--r-- | src/hls/RTLPargenproof.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 05001ce..14220d3 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -41,12 +41,6 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := (STACKS: list_forall2 match_stackframes sf sf'), match_states (RTLBlock.State sf f sp pc rs mem) (RTLPar.State sf' tf sp pc rs mem) -| match_block: - forall sf sf' f tf sp cfi rs mem - (TRANSL: transl_function f = OK tf) - (STACKS: list_forall2 match_stackframes sf sf'), - match_states (RTLBlock.Block sf f sp cfi rs mem) - (RTLPar.Block sf' tf sp (mk_bblock nil cfi) rs mem) | match_returnstate: forall stack stack' v mem (STACKS: list_forall2 match_stackframes stack stack'), |