goto_null_checkt Struct Reference
Return structure for get_null_checked_expr and get_conditional_checked_expr
More...
Collaboration diagram for goto_null_checkt: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. More... | |
| exprt | checked_expr |
| Null-tested pointer expression. More... | |
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
