Skip to content

Commit 4879051

Browse files
committed
Add conversion of null pointer to smt terms
1 parent 7df1571 commit 4879051

File tree

2 files changed

+28
-0
lines changed

2 files changed

+28
-0
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
#include <util/c_types.h>
77
#include <util/expr.h>
88
#include <util/expr_cast.h>
9+
#include <util/expr_util.h>
910
#include <util/floatbv_expr.h>
1011
#include <util/mathematical_expr.h>
1112
#include <util/pointer_expr.h>
@@ -268,6 +269,15 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
268269

269270
static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
270271
{
272+
if(is_null_pointer(constant_literal))
273+
{
274+
const size_t bit_width =
275+
type_checked_cast<pointer_typet>(constant_literal.type()).get_width();
276+
// An address of 0 encodes an object identifier of 0 for the NULL object
277+
// and an offset of 0 into the object.
278+
const auto address = 0;
279+
return smt_bit_vector_constant_termt{address, bit_width};
280+
}
271281
const auto sort = convert_type_to_smt_sort(constant_literal.type());
272282
sort_based_literal_convertert converter(constant_literal);
273283
sort.accept(converter);

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,24 @@ TEST_CASE(
6666
convert_expr_to_smt(from_integer({-1}, signedbv_typet{16})) ==
6767
smt_bit_vector_constant_termt{65535, 16});
6868
}
69+
SECTION("Null pointer")
70+
{
71+
// These config lines are necessary because pointer widths depend on the
72+
// configuration.
73+
config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
74+
config.ansi_c.set_arch_spec_i386();
75+
const smt_termt null_pointer_term =
76+
smt_bit_vector_constant_termt{0, config.ansi_c.pointer_width};
77+
CHECK(
78+
convert_expr_to_smt(null_pointer_exprt{pointer_type(void_type())}) ==
79+
null_pointer_term);
80+
CHECK(
81+
convert_expr_to_smt(null_pointer_exprt{
82+
pointer_type(unsignedbv_typet{100})}) == null_pointer_term);
83+
CHECK(
84+
convert_expr_to_smt(null_pointer_exprt{
85+
pointer_type(pointer_type(void_type()))}) == null_pointer_term);
86+
}
6987
}
7088

7189
TEST_CASE(

0 commit comments

Comments
 (0)