assigns nothing is not possible to proof, if malloc is not in a same function (#2094) · Issues · pub / frama-c