2021-03-03 03:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002485Frama-CPlug-in > wppublic2019-11-08 13:19
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
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 Files
  • c file icon abs.c (238 bytes) 2019-11-08 13:19 -
    
    #include <limits.h>
    
    /*@
        requires INT_MIN < x;
        assigns  \nothing;
        ensures  0 <= x  ==>  \result ==  x;
        ensures  x <  0  ==>  \result == -x;
        ensures  0 <= x*x;
     */
    int abs_int(int x)
    {
        return 0 <= x ? x : -x;
    }
    
    
    
    c file icon abs.c (238 bytes) 2019-11-08 13:19 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-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
+Issue History