wrong proof obligation generated for loop initialization [under why-2.30] (#2097) · Issues · pub / frama-c