2021-01-26 06:30 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002483Frama-CPlug-in > wppublic2019-11-08 12:532019-11-08 12:53
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformLinuxOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0002483: Eprover in Frama-C 20 beta
DescriptionI played a bit with various automatic provers in the beta

alt-ergo (2.3.0), native:alt-ergo (2.3.0), cvc4 (1.6), cvc3 (2.4.1), z3 (4.8.6) are recognized.
Eprover (2.4), on the other hand, is not recognized.

To be honest, Eprover is not such a great prover, but it has helped us discovering inconsistencies in our specifications.
Is there a specific reason, Eprover is not supported?

Attached is the error message.



Steps To Reproduce$ frama-c -wp -wp-rte -wp-prover eprover -wp-out abs.wp abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte] annotating function abs_int
[wp] 6 goals scheduled
[wp] [Eprover 2.4] Goal typed_abs_int_ensures_3 : Failed
  [Why3 Error] Unknown printer 'tptp-fof'
[wp] [Cache] not used
[wp] Proved goals: 5 / 6
  Qed: 5 (0.60ms-3ms-6ms)
  Eprover 2.4: 0 (failed: 1)
TagsNo tags attached.
Attached Files
  • c file icon abs.c (238 bytes) 2019-11-08 12:53 - 
    
#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 12:53 +

-Relationships
+Relationships

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

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