package frama-c

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

Generation of default allocates \nothing clauses.

Automatic generation of allocates \nothing and loop allocates \nothing clauses has been removed until a plugin supports them. To force generation, the following functions can be used.

val add_allocates_nothing_funspec : Cil_types.kernel_function -> unit

Adds allocates \nothing to the default behavior of the function if it does not have and allocation clause yet.

This class adds loop allocates clauses to all the statements it visits.

val add_allocates_nothing : unit -> unit

Add default allocates \nothing clauses to all functions and loops.

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