(** This module adds runtime functions in a [Clight] program. These functions
    implement unsupported functions by the target architecture that introduce a
    branch. We need to define them at the [Clight] level in order to have a
    correct labelling. *)

type operation =
  | Unary of Clight.unary_operation * Clight.ctype
  | Binary of Clight.binary_operation * Clight.ctype * Clight.ctype
  | Cast of Clight.ctype (* destination type *) * Clight.ctype (* source type *)
  | Fun of string (* name of the function *)

type op_replacement =
    (* operation to be replaced *)
    operation *
    (* base name of the replacement function *)
    string *
    (* C definition of the replacement function, provided a name for the
       function *)
    (string -> string) *
    (* dependences *)
    operation list

val add :
  Clight.program -> op_replacement list ->
  (Clight.program * (operation * string) list (* operation association *))

val replace_unsupported : Clight.program -> Clight.program