diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-30 16:52:21 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-30 16:52:21 +0200 |
| commit | 989e85b700161867c2f80df55c2dfaaaa5fe82b4 (patch) | |
| tree | 0e00fd1577a470cfbb19de49926274f8b70abb64 /scheduling/BTL.v | |
| parent | af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 (diff) | |
| download | compcert-kvx-989e85b700161867c2f80df55c2dfaaaa5fe82b4.tar.gz compcert-kvx-989e85b700161867c2f80df55c2dfaaaa5fe82b4.zip | |
BTLtoRTL: proof for internal/external/return states
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 8bdafb89..8529010c 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -451,7 +451,7 @@ Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := | match_stackframe_intro dupmap res f sp pc rs f' pc' (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). Inductive match_states: state -> RTL.state -> Prop := @@ -459,7 +459,7 @@ Inductive match_states: state -> RTL.state -> Prop := dupmap st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) | match_states_call st st' f f' args m |