Frama-C:
Plug-ins:
Libraries:

Frama-C API - WpReached

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