CBMC
local_safe_pointers.cpp File Reference
+ Include dependency graph for local_safe_pointers.cpp:

Go to the source code of this file.

Classes

struct  goto_null_checkt
 Return structure for get_null_checked_expr and get_conditional_checked_expr More...
 

Functions

static optionalt< goto_null_checktget_null_checked_expr (const exprt &expr)
 Check if expr tests if a pointer is null. More...
 

Detailed Description

Local safe pointer analysis

Definition in file local_safe_pointers.cpp.

Function Documentation

◆ get_null_checked_expr()

static optionalt<goto_null_checkt> get_null_checked_expr ( const exprt expr)
static

Check if expr tests if a pointer is null.

Parameters
exprexpression to check
Returns
a goto_null_checkt indicating what expression is tested and whether the check applies on the taken or not-taken branch, or an empty optionalt if this isn't a null check.

Definition at line 37 of file local_safe_pointers.cpp.