Module `Wp.WpReached`Source

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.

Sourceval is_dead_annot : Frama_c_kernel.Cil_types.code_annotation -> bool

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.

Sourceval reachability : Frama_c_kernel.Kernel_function.t -> reachability

memoized reached cfg for function

Sourceval smoking : reachability -> Frama_c_kernel.Cil_types.stmt -> bool

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.

Source

val dump : 
  dir:Frama_c_kernel.Datatype.Filepath.t ->
  Frama_c_kernel.Kernel_function.t ->
  reachability ->
  unit

Sourceval set_doomed : Frama_c_kernel.Emitter.t -> WpPropId.prop_id -> unit

Sourceval unreachable_proved : int ref

Sourceval unreachable_failed : int ref

Sourceval set_unreachable : WpPropId.prop_id -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/WpReached/index.html

Module `Wp.WpReached`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/WpReached/index.html

Module Wp.WpReachedSource

Module `Wp.WpReached`Source