Module E_ACSL.Libc

• 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.