Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002485Frama-CPlug-in > wppublic2019-11-08 13:192019-11-08 13:19
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformLinuxOSxubuntuOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0002485: -wp-out missing output for Why3 provers in Frama-C 20 beta
DescriptionWhen 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?
TagsNo tags attached.
Attached Filesc file icon abs.c [^] (238 bytes) 2019-11-08 13:19 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2019-11-08 13:19 jens New Issue
2019-11-08 13:19 jens Status new => assigned
2019-11-08 13:19 jens Assigned To => correnson
2019-11-08 13:19 jens File Added: abs.c

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker