Module Frama_c_kernel.Logic_to_c

exception No_conversion
val logic_type_to_typ : Cil_types.logic_type -> Cil_types.typ
val logic_var_to_var : Cil_types.logic_var -> Cil_types.varinfo
val loc_lval_to_lval : ?result:Cil_types.varinfo -> Cil_types.term_lval -> Cil_types.lval list
val loc_lhost_to_lhost : ?result:Cil_types.varinfo -> Cil_types.term_lhost -> Cil_types.lhost list
val loc_offset_to_offset : ?result:Cil_types.varinfo -> Cil_types.term_offset -> Cil_types.offset list
val loc_to_exp : ?result:Cil_types.varinfo -> Cil_types.term -> Cil_types.exp list
  • returns

    a list of C expressions.

  • raises No_conversion

    if the argument is not a valid set of expressions.

val loc_to_lval : ?result:Cil_types.varinfo -> Cil_types.term -> Cil_types.lval list
  • returns

    a list of C locations.

  • raises No_conversion

    if the argument is not a valid set of left values.

val loc_to_offset : ?result:Cil_types.varinfo -> Cil_types.term -> Cil_types.offset list
  • returns

    a list of C offset provided the term denotes locations who have all the same base address.

  • raises No_conversion

    if the given term does not match the precondition

val term_lval_to_lval : ?result:Cil_types.varinfo -> Cil_types.term_lval -> Cil_types.lval
val term_to_lval : ?result:Cil_types.varinfo -> Cil_types.term -> Cil_types.lval
val term_to_exp : ?result:Cil_types.varinfo -> Cil_types.term -> Cil_types.exp
val term_offset_to_offset : ?result:Cil_types.varinfo -> Cil_types.term_offset -> Cil_types.offset