CBMC: Member List

is_non_null_at_program_point(const exprt &expr, goto_programt::const_targett program_point) local_safe_pointerst

is_safe_dereference(const dereference_exprt &deref, goto_programt::const_targett program_point) local_safe_pointerst inline

non_null_expressions local_safe_pointerst private

operator()(const goto_programt &goto_program) local_safe_pointerst

output(std::ostream &stream, const goto_programt &program, const namespacet &ns) local_safe_pointerst

output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns) local_safe_pointerst