Module Libc

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 ->
stmt:Cil_types.stmt ->
?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 ~stmt env kf ?result caller args generates code in env to update the memory model after executing the libc function caller with the given args.