Automatic Synthesis of Pointer-Intensive C Programs