fact: Fixpoint extractSome (f : adr -> option adr) (li : list adr) : list adr := match li with | nil => nil | x :: lx => match f x with | Some _ => x :: extractSome f lx | None => extractSome f lx end end.
imports: VST.msl.msl_direct CertiGraph.msl_ext.abs_addr Peano_dec