diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-26 17:30:54 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-26 17:30:54 +0200 |
| commit | f9b7873c679af88533df8ae79468d9a007281fcf (patch) | |
| tree | a5448fb0c2915b1c8fc08c4caf31c67c6aa2f81a /mppa_k1c/Asmblockgenproof.v | |
| parent | 9247603461ccf05167d753e4e023ef5cc692d08d (diff) | |
| download | compcert-kvx-f9b7873c679af88533df8ae79468d9a007281fcf.tar.gz compcert-kvx-f9b7873c679af88533df8ae79468d9a007281fcf.zip | |
Enlèvement du "no_builtin" condition; exec_control sur les option control; exec_straight_blocks
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 345f71b2..fcc32841 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -17,7 +17,7 @@ Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock. (* Require Import Asmgen Asmgenproof0 Asmgenproof1. *) -Require Import Asmblockgen Asmblockgenproof0. +Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1. Module MB := Machblock. Module AB := Asmblock. @@ -1105,7 +1105,7 @@ Proof. set (rs2 := nextblock (bblock_single_inst (Pallocframe (fn_stacksize f) (fn_link_ofs f))) (rs0#FP <- (parent_sp s) #SP <- sp #GPR31 <- Vundef)). destruct TODO. -(* exploit (Pget_correct tge tf GPR8 RA (storeind_ptr GPR8 SP (fn_retaddr_ofs f) x0) rs2 m2'); auto. +(* exploit (Pget_correct tge tf GPR8 RA (storeind_ptr GPR8 SP (fn_retaddr_ofs f) ::b x0) rs2 m2'); auto. intros (rs' & U' & V'). exploit (storeind_ptr_correct tge tf SP (fn_retaddr_ofs f) GPR8 x0 rs' m2'). rewrite chunk_of_Tptr in P. |