Module CSE3analysisaux

module CSE3analysisaux: sig .. end

type flattened_equation_or_condition = 

val flatten_eq : CSE3analysis.equation_or_condition ->
       flattened_equation_or_condition

val imp_add_i_j : HashedSet.PSet.t Maps.PMap.t Stdlib.ref ->
       BinNums.positive -> BinNums.positive -> unit

val string_of_chunk : AST.memory_chunk -> string

val print_reg : Stdlib.out_channel -> int -> unit

val print_eq : 'a -> int * CSE3analysis.sym_op * int list -> unit

val print_cond : 'a -> Op.condition * int list -> unit

val pp_intset : Stdlib.out_channel -> HashedSet.PSet.t -> unit

val pp_rhs : Stdlib.out_channel -> CSE3analysis.sym_op * Camlcoq.P.t list -> unit

val pp_eq : Stdlib.out_channel -> CSE3analysis.equation_or_condition -> unit

val pp_P : Stdlib.out_channel -> Camlcoq.P.t -> unit

val pp_option : (Stdlib.out_channel -> 'a -> unit) -> Stdlib.out_channel -> 'a option -> unit

val is_trivial : CSE3analysis.equation_or_condition -> bool

val pp_list : string ->
       (Stdlib.out_channel -> 'a -> unit) -> Stdlib.out_channel -> 'a list -> unit

val pp_set : string ->
       (Stdlib.out_channel -> BinNums.positive -> unit) ->
       Stdlib.out_channel -> HashedSet.PSet.t -> unit

val pp_equation : CSE3analysis.analysis_hints -> Stdlib.out_channel -> BinNums.positive -> unit

val pp_relation : CSE3analysis.analysis_hints -> Stdlib.out_channel -> HashedSet.PSet.t -> unit

val pp_relation_b : CSE3analysis.analysis_hints ->
       Stdlib.out_channel -> HashedSet.PSet.t option -> unit

val pp_results : RTL.coq_function ->
       CSE3analysis.RB.t Maps.PMap.t ->
       CSE3analysis.analysis_hints -> Stdlib.out_channel -> unit

module IntSet: Stdlib.Set.Make(sig

type t = int 

val compare : int -> int -> int

end)

val union_list : CSE3analysis.RB.t -> CSE3analysis.RB.t list -> CSE3analysis.RB.t

val rb_glb : CSE3analysis.RB.t -> CSE3analysis.RB.t -> CSE3analysis.RB.t

val compute_invariants : RTL.node list ->
       RTL.node ->
       (RTL.node -> CSE3analysis.RB.t -> (RTL.node * CSE3analysis.RB.t) list) ->
       CSE3analysis.RB.t * CSE3analysis.RB.t Maps.PTree.tree

val refine_invariants : RTL.node list ->
       RTL.node ->
       (RTL.node -> RTL.node list) ->
       (RTL.node -> RTL.node list) ->
       (RTL.node -> CSE3analysis.RB.t -> (RTL.node * CSE3analysis.RB.t) list) ->
       CSE3analysis.RB.t Maps.PMap.t -> CSE3analysis.RB.t Maps.PMap.t

val get_default : 'a -> BinNums.positive -> 'a Maps.PTree.tree -> 'a

val initial_analysis : CSE3analysis.eq_context ->
       CSE3analysis.typing_env ->
       RTL.coq_function -> CSE3analysis.RB.t * CSE3analysis.RB.t Maps.PTree.tree

val refine_analysis : CSE3analysis.eq_context ->
       CSE3analysis.typing_env ->
       RTL.coq_function ->
       CSE3analysis.RB.t Maps.PMap.t -> CSE3analysis.RB.t Maps.PMap.t

val add_to_set_in_table : ('a, HashedSet.PSet.t) Stdlib.Hashtbl.t -> 'a -> BinNums.positive -> unit

val preanalysis : CSE3analysis.typing_env ->
       RTL.coq_function ->
       CSE3analysis.RB.t Maps.PMap.t * CSE3analysis.analysis_hints