From fe903fdf03453a478303fe51551a4a0ea72d4b5d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 19 Feb 2022 13:03:03 +0000 Subject: [PATCH] Remove Throwing-NULL check from goto_check_ct This check was introduced in d2713b200, 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. It was, however, only intended for the Java front-end: for the C language, "throw" is not relevant, and C++ permits throwing NULL. Therefore, remove this check from goto_check_ct. --- src/analyses/goto_check_c.cpp | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index d07bbbd7b34..41bcc05fc7e 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -2170,27 +2170,6 @@ void goto_check_ct::goto_check( } else if(i.is_throw()) { - if( - i.get_code().get_statement() == ID_expression && - i.get_code().operands().size() == 1 && - i.get_code().op0().operands().size() == 1) - { - // must not throw NULL - - exprt pointer = to_unary_expr(i.get_code().op0()).op(); - - const notequal_exprt not_eq_null( - pointer, null_pointer_exprt(to_pointer_type(pointer.type()))); - - add_guarded_property( - not_eq_null, - "throwing null", - "pointer dereference", - i.source_location(), - pointer, - identity); - } - // this has no successor assertions.clear(); }