Wp.WpReachedSourceReachability for Smoke Tests
control flow graph dedicated to smoke tests
If returns true the predicate has always the given boolean value.
False assertions and loop invariant. Hence, also includes completely unrolled loop.
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 dump :
dir:Frama_c_kernel.Datatype.Filepath.t ->
Frama_c_kernel.Kernel_function.t ->
reachability ->
unit