search

Frama-C / Frama-C-snapshot

Release snapshots of the Frama-C platform for source code analysis
http://frama-c.com
167 stars 38 forks source link

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

Closed jensgerlach closed 5 years ago

jensgerlach commented 5 years ago

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 commented 5 years ago

See BTS entry for more details.

jensgerlach commented 5 years ago

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