Frama-C API - WpReached
Reachability for 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.
val reachability : Frama_c_kernel.Kernel_function.t -> reachability
memoized reached cfg for function
val 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.
val dump : dir:Frama_c_kernel.Datatype.Filepath.t -> Frama_c_kernel.Kernel_function.t -> reachability -> unit
val set_doomed : Frama_c_kernel.Emitter.t -> WpPropId.prop_id -> unit
val set_unreachable : WpPropId.prop_id -> unit