-
Notifications
You must be signed in to change notification settings - Fork 262
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Move is_null_pointer to constant_exprt
Removes one of the functions from the expr_util translation unit that is supposed to be deprecated.
- Loading branch information
1 parent
4ae54e6
commit 42b70b2
Showing
27 changed files
with
62 additions
and
57 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected] | |
#include <util/c_types.h> | ||
#include <util/config.h> | ||
#include <util/cprover_prefix.h> | ||
#include <util/expr_util.h> | ||
#include <util/find_symbols.h> | ||
#include <util/fixedbv.h> | ||
#include <util/floatbv_expr.h> | ||
|
@@ -1983,7 +1982,7 @@ std::string expr2ct::convert_constant( | |
} | ||
else if(type.id()==ID_pointer) | ||
{ | ||
if(is_null_pointer(src)) | ||
if(src.is_null_pointer()) | ||
{ | ||
if(configuration.use_library_macros) | ||
dest = "NULL"; | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected] | |
#include <util/bitvector_expr.h> | ||
#include <util/byte_operators.h> | ||
#include <util/c_types.h> | ||
#include <util/expr_util.h> | ||
#include <util/format_expr.h> | ||
#include <util/format_type.h> | ||
#include <util/namespace.h> | ||
|
@@ -621,7 +620,7 @@ void value_sett::get_value_set_rec( | |
else if(expr.is_constant()) | ||
{ | ||
// check if NULL | ||
if(is_null_pointer(to_constant_expr(expr))) | ||
if(to_constant_expr(expr).is_null_pointer()) | ||
{ | ||
insert( | ||
dest, | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected] | |
#include <util/arith_tools.h> | ||
#include <util/byte_operators.h> | ||
#include <util/c_types.h> | ||
#include <util/expr_util.h> | ||
#include <util/namespace.h> | ||
#include <util/pointer_expr.h> | ||
#include <util/simplify_expr.h> | ||
|
@@ -532,7 +531,7 @@ void value_set_fit::get_value_set_rec( | |
else if(expr.is_constant()) | ||
{ | ||
// check if NULL | ||
if(is_null_pointer(to_constant_expr(expr))) | ||
if(to_constant_expr(expr).is_null_pointer()) | ||
{ | ||
insert( | ||
dest, | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected] | |
#include <util/c_types.h> | ||
#include <util/config.h> | ||
#include <util/exception_utils.h> | ||
#include <util/expr_util.h> | ||
#include <util/namespace.h> | ||
#include <util/pointer_expr.h> | ||
#include <util/pointer_offset_size.h> | ||
|
@@ -443,7 +442,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) | |
{ | ||
const constant_exprt &c = to_constant_expr(expr); | ||
|
||
if(is_null_pointer(c)) | ||
if(c.is_null_pointer()) | ||
return encode(pointer_logic.get_null_object(), type); | ||
else | ||
{ | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected] | |
* \date Sun Jul 31 21:54:44 BST 2011 | ||
*/ | ||
|
||
#include "deprecate.h" | ||
#include "irep.h" | ||
|
||
#include <functional> | ||
|
@@ -116,6 +117,7 @@ exprt make_and(exprt a, exprt b); | |
/// Returns true if \p expr has a pointer type and a value NULL; it also returns | ||
/// true when \p expr has value zero and NULL_is_zero is true; returns false in | ||
/// all other cases. | ||
DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_null_pointer() instead")) | ||
bool is_null_pointer(const constant_exprt &expr); | ||
|
||
#endif // CPROVER_UTIL_EXPR_UTIL_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.