Module Generic.Build

module Build: Va_build

val function_declaration : loc:Cil_types.location ->
string ->
Cil_types.typ ->
(Cil_types.varinfo list -> Cil_types.funspec) ->
Cil_types.varinfo * Cil_types.global
val vi_assign : loc:Cil_types.location ->
Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt
val array_assign : loc:Cil_types.location ->
Cil_types.varinfo -> Cil_types.exp list -> Cil_types.stmt list
val array_init : loc:Cil_types.location ->
Cil_types.fundec ->
Cil_types.block ->
string ->
Cil_types.typ ->
Cil_types.exp list -> Cil_types.varinfo * Cil_types.stmt list
val call : loc:Cil_types.location ->
Cil_types.lval option ->
Cil_types.varinfo -> Cil_types.exp list -> Cil_types.stmt
val read : loc:Cil_types.location -> Cil_types.exp -> Cil_types.stmt
val logic_elval : loc:Cil_datatype.Location.t -> Cil_types.term_lval -> Cil_types.term
val logic_var : Cil_types.varinfo -> Cil_types.term_lhost * Cil_types.term_offset
val logic_evar : loc:Cil_datatype.Location.t -> Cil_types.varinfo -> Cil_types.term
val logic_varmem : loc:Cil_datatype.Location.t ->
Cil_types.varinfo -> Cil_types.term_lhost * Cil_types.term_offset
val logic_varfield : loc:Cil_datatype.Location.t ->
Cil_types.varinfo ->
Cil_types.fieldinfo -> Cil_types.term_lhost * Cil_types.term_offset
val logic_varrange : loc:Cil_datatype.Location.t ->
Cil_types.varinfo -> Cil_types.term_lhost * Cil_types.term_offset
val logic_return : Cil_types.typ -> Cil_types.term_lhost * Cil_types.term_offset