rule <k> #memory [ ret _ ] => . ... </k> <localCalls> .List </localCalls>
and
rule <k> #memory [ ret ARGS ] => #memoryDelta(0 -Int intSizes(REGS, NREGS) -Int Gcallmemory < SCHED >) ... </k> <schedule> SCHED </schedule> <fid> NAME </fid> <regs> REGS </regs><funcId> NAME </funcId><nregs> NREGS </nregs> overlaps.
The second rule needs to check localCalls is not empty.
rule <k> #memory [ ret _ ] => . ... </k> <localCalls> .List </localCalls>and
rule <k> #memory [ ret ARGS ] => #memoryDelta(0 -Int intSizes(REGS, NREGS) -Int Gcallmemory < SCHED >) ... </k> <schedule> SCHED </schedule> <fid> NAME </fid> <regs> REGS </regs><funcId> NAME </funcId><nregs> NREGS </nregs>overlaps.The second rule needs to check localCalls is not empty.