Frama-C:
Plug-ins:
Libraries:

Frama-C API - Libc

Code generation for libc functions

val is_writing_memory : Frama_c_kernel.Cil_types.varinfo -> bool
  • returns

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

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.