File tree Expand file tree Collapse file tree 1 file changed +0
-21
lines changed
Expand file tree Collapse file tree 1 file changed +0
-21
lines changed Original file line number Diff line number Diff line change @@ -2170,27 +2170,6 @@ void goto_check_ct::goto_check(
21702170 }
21712171 else if (i.is_throw ())
21722172 {
2173- if (
2174- i.get_code ().get_statement () == ID_expression &&
2175- i.get_code ().operands ().size () == 1 &&
2176- i.get_code ().op0 ().operands ().size () == 1 )
2177- {
2178- // must not throw NULL
2179-
2180- exprt pointer = to_unary_expr (i.get_code ().op0 ()).op ();
2181-
2182- const notequal_exprt not_eq_null (
2183- pointer, null_pointer_exprt (to_pointer_type (pointer.type ())));
2184-
2185- add_guarded_property (
2186- not_eq_null,
2187- " throwing null" ,
2188- " pointer dereference" ,
2189- i.source_location (),
2190- pointer,
2191- identity);
2192- }
2193-
21942173 // this has no successor
21952174 assertions.clear ();
21962175 }
You can’t perform that action at this time.
0 commit comments