diff options
| author | Cyril SIX <cyril.six@univ-grenoble-alpes.fr> | 2019-10-11 11:49:31 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@univ-grenoble-alpes.fr> | 2019-10-11 11:49:31 +0200 |
| commit | 75326127cbb4d57d435b28651ef65dcd2a0b8ce5 (patch) | |
| tree | 7db6a37fd180c8146e6390943d5748d48819cf38 /mppa_k1c/Asmblockgen.v | |
| parent | 45e689e558d839b512d39b0e25083b5928f5dd58 (diff) | |
| download | compcert-kvx-75326127cbb4d57d435b28651ef65dcd2a0b8ce5.tar.gz compcert-kvx-75326127cbb4d57d435b28651ef65dcd2a0b8ce5.zip | |
Fixing fp_is_parent too weak (#165)
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ade84e7b..bbe24fec 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -1111,10 +1111,12 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := match i with + | MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP) | MBsetstack src ofs ty => before | MBgetparam ofs ty dst => negb (mreg_eq dst MFP) | MBop op args res => before && negb (mreg_eq res MFP) - | _ => false + | MBload chunk addr args dst => before && negb (mreg_eq dst MFP) + | MBstore chunk addr args res => before end. (** This is the naive definition, which is not tail-recursive unlike the other backends *) |