Module Libc

module Libc: sig .. end

Code generation for libc functions

val is_writing_memory : Cil_types.varinfo -> bool

Returns true if the function is a libc function that writes memory.

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.

Returns a tuple result_opt, env where result_opt is an option with the lvalue for the result of the function and env is the updated environement.