package frama-c

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

    if kf has no definition.

  • returns

    3 statement sets related to the value of lval before stmt :

    • the forward selection,
    • the both way selection,
    • the backward selection.

compute the set of statements where the given annotation has the same value as before the given stmt. Also returns the eventual code annotations that are implied by the one given as argument.

val check_asserts : unit -> Frama_c_kernel.Cil_types.code_annotation list

Print how many assertions could be removed based on the previous analysis (get_prop_scope_at_stmt) and return the annotations that can be removed.

val rm_asserts : unit -> unit

Same analysis than check_asserts but mark the assertions as proven.

for internal use

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