package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.