diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-05 15:15:48 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:59:07 +0200 |
| commit | 672d9ea4489158f6a6b7175463c6514a91d1490d (patch) | |
| tree | bd358992610110b8c7ebdefb5979ef30f601215a /driver | |
| parent | 5a78e28f0bd7e8f822d96c4ad24ab20cca8fedd1 (diff) | |
| download | compcert-kvx-672d9ea4489158f6a6b7175463c6514a91d1490d.tar.gz compcert-kvx-672d9ea4489158f6a6b7175463c6514a91d1490d.zip | |
Rajout d'un return_address_offset. Besoin de changer forward_simu de mach machblock
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..1cb5bd36 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -404,7 +404,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct. eapply compose_forward_simulations. - eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset). + eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof.return_address_offset). exact Asmgenproof.return_address_exists. eassumption. eapply Asmgenproof.transf_program_correct; eassumption. |