Skip to content

Commit bae7653

Browse files
committed
Throwing-NULL check should only be triggered by --pointer-check
This check was introduced in d2713b2, with no particular reason that it should be enabled unconditionally. The test included in that commit has --pointer-check set, suggesting that this always was the desired behaviour.
1 parent 79c1637 commit bae7653

File tree

3 files changed

+11
-2
lines changed

3 files changed

+11
-2
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
NullPointer3
3+
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
^.*Null pointer check: FAILURE$

jbmc/src/java_bytecode/goto_check_java.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1447,7 +1447,7 @@ void goto_check_javat::goto_check(
14471447
else if(i.is_throw())
14481448
{
14491449
if(
1450-
i.get_code().get_statement() == ID_expression &&
1450+
enable_pointer_check && i.get_code().get_statement() == ID_expression &&
14511451
i.get_code().operands().size() == 1 &&
14521452
i.get_code().op0().operands().size() == 1)
14531453
{

src/analyses/goto_check_c.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2171,7 +2171,7 @@ void goto_check_ct::goto_check(
21712171
else if(i.is_throw())
21722172
{
21732173
if(
2174-
i.get_code().get_statement() == ID_expression &&
2174+
enable_pointer_check && i.get_code().get_statement() == ID_expression &&
21752175
i.get_code().operands().size() == 1 &&
21762176
i.get_code().op0().operands().size() == 1)
21772177
{

0 commit comments

Comments
 (0)