WP: number of generated files in Frama-C 18 vs 19. beta(2)

[jensgerlach]

There are some difficult to understand (internal) differences in the verification of the rotate_copy example from here.

Both 18.0 and 19 beta2 report the discharge of the 17 proof obligations of rotate_copy with reporting 5 discharged Qed and the remaining 12 by Alt-Ergo.

Frama-C 18.0 generates 12 .mlw and .out files.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged.

[jensgerlach]

See BTS entry for more details.

[jensgerlach]

This issue has apparently been fixed in the final release of 19.0