Skip to content

Commit 659ca2c

Browse files
author
Owen
committed
Use is_invalid_pointer_exprt directly
1 parent 885daa6 commit 659ca2c

File tree

4 files changed

+7
-15
lines changed

4 files changed

+7
-15
lines changed

src/analyses/goto_check.cpp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1129,18 +1129,16 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
11291129

11301130
if(flags.is_unknown())
11311131
{
1132-
conditions.push_back(
1133-
conditiont(not_exprt(is_invalid_pointer(address)), "pointer invalid"));
1132+
conditions.push_back(conditiont{
1133+
not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
11341134
}
11351135

11361136
if(flags.is_uninitialized())
11371137
{
11381138
conditions.push_back(
1139-
conditiont(
1140-
or_exprt(
1141-
in_bounds_of_some_explicit_allocation,
1142-
not_exprt(is_invalid_pointer(address))),
1143-
"pointer uninitialized"));
1139+
conditiont{or_exprt{in_bounds_of_some_explicit_allocation,
1140+
not_exprt{is_invalid_pointer_exprt{address}}},
1141+
"pointer uninitialized"});
11441142
}
11451143

11461144
if(flags.is_unknown() || flags.is_dynamic_heap())

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2104,7 +2104,7 @@ exprt c_typecheck_baset::do_special_functions(
21042104
throw 0;
21052105
}
21062106

2107-
exprt same_object_expr = is_invalid_pointer(expr.arguments().front());
2107+
exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()};
21082108
same_object_expr.add_source_location()=source_location;
21092109

21102110
return same_object_expr;

src/util/pointer_predicates.cpp

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ exprt good_pointer_def(
105105

106106
const not_exprt not_null(null_pointer(pointer));
107107

108-
const not_exprt not_invalid(is_invalid_pointer(pointer));
108+
const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
109109

110110
const or_exprt bad_other(
111111
object_lower_bound(pointer, nil_exprt()),
@@ -139,11 +139,6 @@ exprt null_pointer(const exprt &pointer)
139139
return same_object(pointer, null_pointer);
140140
}
141141

142-
exprt is_invalid_pointer(const exprt &pointer)
143-
{
144-
return is_invalid_pointer_exprt{pointer};
145-
}
146-
147142
exprt dynamic_object_lower_bound(
148143
const exprt &pointer,
149144
const exprt &offset)

src/util/pointer_predicates.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@ exprt good_pointer_def(const exprt &pointer, const namespacet &);
3333
exprt null_object(const exprt &pointer);
3434
exprt null_pointer(const exprt &pointer);
3535
exprt integer_address(const exprt &pointer);
36-
exprt is_invalid_pointer(const exprt &pointer);
3736
exprt dynamic_object_lower_bound(
3837
const exprt &pointer,
3938
const exprt &offset);

0 commit comments

Comments
 (0)