src/clight/runtime.mli

   1
   2 (** This module adds runtime functions in a [Clight] program. These functions
   3     implement unsupported functions by the target architecture that introduce a
   4     branch. We need to define them at the [Clight] level in order to have a
   5     correct labelling. *)
   6
   7 type operation =
   8   | Unary of Clight.unary_operation * Clight.ctype
   9   | Binary of Clight.binary_operation * Clight.ctype * Clight.ctype
  10   | Cast of Clight.ctype (* destination type *) * Clight.ctype (* source type *)
  11   | Fun of string (* name of the function *)
  12
  13 type op_replacement =
  14     (* operation to be replaced *)
  15     operation *
  16     (* base name of the replacement function *)
  17     string *
  18     (* C definition of the replacement function, provided a name for the
  19        function *)
  20     (string -> string) *
  21     (* dependences *)
  22     operation list
  23
  24 val add :
  25   Clight.program -> op_replacement list ->
  26   (Clight.program * (operation * string) list (* operation association *))
  27
  28 val replace_unsupported : Clight.program -> Clight.program