E_ACSL.Logic_array
val comparison_to_exp :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.kernel_function ->
Env.t ->
name:string ->
Frama_c_kernel.Cil_types.binop ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.t
comparison_to_exp ~loc kf env ~name bop e1 e2
generate the C code equivalent to e1 bop e2
. Requires that bop
is either Ne
or Eq
and that e1
and e2
are arrays.
val translate_rte_ref :
(?filter:(Frama_c_kernel.Cil_types.code_annotation -> bool) ->
Frama_c_kernel.Cil_types.kernel_function ->
Env.t ->
Frama_c_kernel.Cil_types.exp ->
Env.t)
Stdlib.ref