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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct