E_ACSL.Libc
Code generation for libc functions
val is_writing_memory : Frama_c_kernel.Cil_types.varinfo -> bool
val update_memory_model :
loc:Frama_c_kernel.Cil_types.location ->
?result:Frama_c_kernel.Cil_types.lval ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.Cil_types.exp list ->
Frama_c_kernel.Cil_types.lval option * Env.t
update_memory_model ~loc env kf ?result caller args
generates code in env
to update the memory model after executing the libc function caller
with the given args
.