package frama-c

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

Module Wp.WpReachedSource

Reachability for Smoke Tests

Sourcetype reachability

control flow graph dedicated to smoke tests

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

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

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

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

Sourceval unreachable_proved : int ref
Sourceval unreachable_failed : int ref
Sourceval 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