Module type Sig.With_Fixpoint_Computation

module Context : Context

val mu_context_open : Context.t -> Context.t

Opening a new context can also be seen as opening a new scope: new variables can be introduced, but variables of the parent scope can still be seen.

val typed_fixpoint_step : iteration:int -> init:Context.t -> arg:Context.t -> body:Context.t -> (bool * 'a Context.in_tuple) -> bool * (close:bool -> 'a Context.out_tuple * Context.t)

Fixpoint step is a combination of inclusion checking + widening.

• parameter init

  is the context leading to the loop entry,

• parameter arg

  is the context at the loop entry (obtained by mu_context_open or by the last fixpoint_step operation)

• parameter body

  is the context at the end of the loop

Also takes a boolean and a tuple of values which is the result of the evaluation of the body (the end of the loop).

Internally, it stores the arguments of the mu.

• returns

  a boolean which says if the fixpoint is reached, and a function. If the fixpoint is reached, we can "close" the mu, and the function returns a tuple corresponding to the mu. We can always "restart" the mu, in which case the function returns a new arg.

val widened_fixpoint_step : widening_id:Widening_Id.t -> previous:Context.t -> next:Context.t -> (bool * 'a Context.in_tuple) -> Context.t * bool * 'a Context.out_tuple

widened_fixpoint_step ~previous ~next (bool,in_tuple) where:

• widening_id is a unique representation of the widening point;
• previous is the previous domain state;
• next is the next domain state obtained after execution of the function body;
• bool is false if we know that the fixpoint is not reached yet, and true otherwise;
• in_tuple is the argument of the SSA phi function;

returns a triple (context,bool,out_tuple) where:

• context is the new domain state;
• bool is true if the fixpoint is reached, and false if not reached or we don't know;
• out_tuple is the result of the SSA phi function.