| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002483 | Frama-C | Plug-in > wp | public | 2019-11-08 12:53 | 2019-11-08 12:53 |
|
| Reporter | jens | |
| Assigned To | correnson | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | assigned | Resolution | open | |
| Platform | Linux | OS | | OS Version | |
| Product Version | Frama-C GIT, precise the release id | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0002483: Eprover in Frama-C 20 beta |
| Description | I 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)
|
| Tags | No tags attached. |
|
| Attached Files |  abs.c [^] (238 bytes) 2019-11-08 12:53 [Show Content] [Hide Content]
#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;
}
|
|
Relationships 
Relationships