From 4b0a2d6f3c71fd2e89dd2b8133949043f8837bfd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 May 2018 08:17:28 +0000 Subject: [PATCH] goto_check: do not unnecessarily build size-of expressions Before, the member offset would be computed even when no (pointer) checks were enabled. This is unnecessary overhead; skipping over this reduces execution time on compiled Linux kernel binaries from 15 minutes to 6 minutes. --- src/analyses/goto_check.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 27d5fc318da..cbc93c75968 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1383,6 +1383,11 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address) check_rec(deref.op0(), guard, false); + // avoid building the following expressions when pointer_validity_check + // would return immediately anyway + if(!enable_pointer_check) + return; + exprt access_ub=nil_exprt(); exprt member_offset=member_offset_expr(member, ns);