Frama-C Bug Tracking System - Frama-C
View Issue Details
0002485Frama-CPlug-in > wppublic2019-11-08 13:192019-11-08 13:19
normalminorhave not tried
Frama-C GIT, precise the release id 
0002485: -wp-out missing output for Why3 provers in Frama-C 20 beta
When the attached programme is processed with frama-c -wp -wp-rte -wp-prover native:alt-ergo -wp-out abs.wp abs.c then the output directory 'abs.wp/typed' contains three files abs_ensures_3_Alt-Ergo.mlw abs_ensures_3_Alt-Ergo.out abs_ensures_3.ergo When using the command line frama-c -wp -wp-rte -wp-prover alt-ergo -wp-out abs.wp abs.c then the output directory 'abs.wp/typed' contains only the generated proof obligation abs_ensures_3_Why3_Alt_Ergo_2_3_0.why (similiarly when using another Why3 prover, such as cvc4) Is there a way to output also the result for Why3 provers?
No tags attached.
c abs.c (238) 2019-11-08 13:19
Issue History
2019-11-08 13:19jensNew Issue
2019-11-08 13:19jensStatusnew => assigned
2019-11-08 13:19jensAssigned To => correnson
2019-11-08 13:19jensFile Added: abs.c

There are no notes attached to this issue.