Loading...

Searching...

No Matches

Public Attributes | List of all members

goto_null_checkt Struct Reference

Return structure for get_null_checked_expr and get_conditional_checked_expr More...

+ Collaboration diagram for goto_null_checkt:

[フレーム]

[legend]

Public Attributes

bool checked_when_taken

If true, the given GOTO/ASSUME tests that a pointer expression is non-null on the taken branch or passing case; otherwise, on the not-taken branch or on failure.

exprt checked_expr

Null-tested pointer expression.

Detailed Description

Return structure for get_null_checked_expr and get_conditional_checked_expr

Definition at line 20 of file local_safe_pointers.cpp.

Member Data Documentation

◆ checked_expr

exprt goto_null_checkt::checked_expr

Null-tested pointer expression.

Definition at line 28 of file local_safe_pointers.cpp.

◆ checked_when_taken

bool goto_null_checkt::checked_when_taken

If true, the given GOTO/ASSUME tests that a pointer expression is non-null on the taken branch or passing case; otherwise, on the not-taken branch or on failure.

Definition at line 25 of file local_safe_pointers.cpp.

The documentation for this struct was generated from the following file:

/home/runner/work/cbmc/cbmc/src/analyses/local_safe_pointers.cpp