diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
| commit | 271f87ba08f42340900378c0797511d4071fc1b8 (patch) | |
| tree | 8b861fa3221b179bb8e3ad339864cdb7c541d46a /driver | |
| parent | e6a1df51a2a3d29c58d72453355e50a979e86297 (diff) | |
| download | compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.tar.gz compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.zip | |
BTL Scheduler oracle and some drafts
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.vexpand | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 85f265db..40ea0d68 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -300,7 +300,7 @@ EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. eapply RTLtoBTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply BTLtoRTLproof.transf_program_correct_cfg; eassumption. + eapply BTLtoRTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. |