module Libc:sig
..end
Code generation for libc functions
Code generation for libc functions
val is_writing_memory : Cil_types.varinfo -> bool
val update_memory_model : loc:Cil_types.location ->
?result:Cil_types.lval ->
Env.t ->
Cil_types.kernel_function ->
Cil_types.varinfo -> Cil_types.exp list -> 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
.
result_opt, env
where result_opt
is an option with
the lvalue for the result of the function and env
is the updated
environement.