functor (W : Mcfg.S->
  sig
    val process_global_init :
      W.t_env -> Cil_types.kernel_function -> W.t_prop -> W.t_prop
  end