package frama-c

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

Reachability for Smoke Tests

type reachability

control flow graph dedicated to smoke tests

val is_predicate : bool -> Frama_c_kernel.Cil_types.predicate -> bool

If returns true the predicate has always the given boolean value.

val is_dead_annot : Frama_c_kernel.Cil_types.code_annotation -> bool

False assertions and loop invariant. Hence, also includes completely unrolled loop.

val is_dead_code : Frama_c_kernel.Cil_types.stmt -> bool

Checks whether the stmt has a dead-code annotation.

memoized reached cfg for function

Returns whether a stmt need a smoke tests to avoid being unreachable. This is restricted to assignments, returns and calls not dominated another smoking statement.

val set_doomed : Frama_c_kernel.Emitter.t -> WpPropId.prop_id -> unit
val unreachable_proved : int Stdlib.ref
val unreachable_failed : int Stdlib.ref
val set_unreachable : WpPropId.prop_id -> unit
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