@@ -992,12 +992,16 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
992
992
alloc_disjuncts.push_back (and_exprt (lb_check, ub_check));
993
993
}
994
994
995
- const exprt allocs = disjunction (alloc_disjuncts);
995
+ const exprt in_bounds_of_some_explicit_allocation =
996
+ disjunction (alloc_disjuncts);
996
997
997
998
if (flags.is_unknown () || flags.is_null ())
998
999
{
999
1000
conditions.push_back (conditiont (
1000
- or_exprt (allocs, not_exprt (null_pointer (address))), " pointer NULL" ));
1001
+ or_exprt (
1002
+ in_bounds_of_some_explicit_allocation,
1003
+ not_exprt (null_pointer (address))),
1004
+ " pointer NULL" ));
1001
1005
}
1002
1006
1003
1007
if (flags.is_unknown ())
@@ -1010,21 +1014,28 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
1010
1014
if (flags.is_uninitialized ())
1011
1015
{
1012
1016
conditions.push_back (conditiont (
1013
- or_exprt (allocs, not_exprt (invalid_pointer (address))),
1017
+ or_exprt (
1018
+ in_bounds_of_some_explicit_allocation,
1019
+ not_exprt (invalid_pointer (address))),
1014
1020
" pointer uninitialized" ));
1015
1021
}
1016
1022
1017
1023
if (flags.is_unknown () || flags.is_dynamic_heap ())
1018
1024
{
1019
1025
conditions.push_back (conditiont (
1020
- or_exprt (allocs, not_exprt (deallocated (address, ns))),
1026
+ or_exprt (
1027
+ in_bounds_of_some_explicit_allocation,
1028
+ not_exprt (deallocated (address, ns))),
1021
1029
" deallocated dynamic object" ));
1022
1030
}
1023
1031
1024
1032
if (flags.is_unknown () || flags.is_dynamic_local ())
1025
1033
{
1026
1034
conditions.push_back (conditiont (
1027
- or_exprt (allocs, not_exprt (dead_object (address, ns))), " dead object" ));
1035
+ or_exprt (
1036
+ in_bounds_of_some_explicit_allocation,
1037
+ not_exprt (dead_object (address, ns))),
1038
+ " dead object" ));
1028
1039
}
1029
1040
1030
1041
if (flags.is_unknown () || flags.is_dynamic_heap ())
@@ -1035,7 +1046,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
1035
1046
1036
1047
conditions.push_back (conditiont (
1037
1048
or_exprt (
1038
- allocs ,
1049
+ in_bounds_of_some_explicit_allocation ,
1039
1050
implies_exprt (
1040
1051
malloc_object (address, ns), not_exprt (dynamic_bounds_violation))),
1041
1052
" pointer outside dynamic object bounds" ));
@@ -1051,7 +1062,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
1051
1062
1052
1063
conditions.push_back (conditiont (
1053
1064
or_exprt (
1054
- allocs ,
1065
+ in_bounds_of_some_explicit_allocation ,
1055
1066
implies_exprt (
1056
1067
not_exprt (dynamic_object (address)),
1057
1068
not_exprt (object_bounds_violation))),
@@ -1061,7 +1072,8 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
1061
1072
if (flags.is_unknown () || flags.is_integer_address ())
1062
1073
{
1063
1074
conditions.push_back (conditiont (
1064
- implies_exprt (integer_address (address), allocs),
1075
+ implies_exprt (
1076
+ integer_address (address), in_bounds_of_some_explicit_allocation),
1065
1077
" invalid integer address" ));
1066
1078
}
1067
1079
0 commit comments