Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs