Skip to content

Commit 4b0a2d6

Browse files
committed
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.
1 parent 40ecff8 commit 4b0a2d6

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/analyses/goto_check.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -1383,6 +1383,11 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
13831383

13841384
check_rec(deref.op0(), guard, false);
13851385

1386+
// avoid building the following expressions when pointer_validity_check
1387+
// would return immediately anyway
1388+
if(!enable_pointer_check)
1389+
return;
1390+
13861391
exprt access_ub=nil_exprt();
13871392

13881393
exprt member_offset=member_offset_expr(member, ns);

0 commit comments

Comments
 (0)