PPO (* Computes ppo the ARM and PPC way *) (* Fixpoint from i -> c in instructions and transitivity *) let rec ci = ci0 | (ci;ii) | (cc;ci) and ii = ii0 | ci | (ic;ci) | (ii;ii) and cc = cc0 | ci | (ci;ic) | (cc;cc) and ic = ic0 | ii | cc | (ic;cc) | (ii ; ic) (* | ci inclus dans ii et cc *) let ppo = let ppoR = ii & (R * R) and ppoW = ic & (R * W) in ppoR | ppoW