diff options
Diffstat (limited to 'powerpc/Constprop.v')
| -rw-r--r-- | powerpc/Constprop.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v index 75fb1486..6ec27a3f 100644 --- a/powerpc/Constprop.v +++ b/powerpc/Constprop.v @@ -654,8 +654,10 @@ Definition transfer (f: function) (pc: node) (before: D.t) := D.set res Unknown before | Itailcall sig ros args => before +(* | Ialloc arg res s => D.set res Unknown before +*) | Icond cond args ifso ifnot => before | Ireturn optarg => @@ -1045,8 +1047,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) := Icall sig (transf_ros approx ros) args res s | Itailcall sig ros args => Itailcall sig (transf_ros approx ros) args - | Ialloc arg res s => - Ialloc arg res s | Icond cond args s1 s2 => match eval_static_condition cond (approx_regs args approx) with | Some b => |