2021-02-24 18:54 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002380Frama-CPlug-in > wppublic2018-11-30 10:40
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in VersionFrama-C 17-Chlorine 
Summary0002380: `strlen` used from code makes it no longer possible to prove `assigns \nothing`.
Description`strlen` used from code makes it no longer possible to prove `assigns \nothing`. The definition in the Frama-C library has `@ assigns \result \from indirect:s[0..];`, but this should not prevent check?
Steps To Reproduce$ cat bug.c
#include <string.h>

requires strlen(s)>=0 && \valid(s+(0..strlen(s)));
assigns \nothing;
int len(char *s) {
  return strlen(s);

$ frama-c -wp -wp-rte -wp-prover CVC4,alt-ergo bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function len
[wp] 5 goals scheduled
[wp] [Failed] Goal typed_len_assign_normal_part1
        CVC4: Timeout (Qed:2ms) (10s)
    Alt-Ergo: Unknown (Qed:2ms) (324ms)
[wp] [Failed] Goal typed_len_assign_exit
        CVC4: Timeout (Qed:2ms) (10s)
    Alt-Ergo: Unknown (Qed:2ms) (322ms)
[wp] Proved goals: 3 / 5
    Qed: 2 (0.35ms-0.85ms-2ms)
    Alt-Ergo: 1 (15ms) (20) (unknown: 2)
    CVC4: 0 (interrupted: 2)
TagsNo tags attached.
Attached Files




correnson (manager)

The bug is not reproducible under Frama-C Chlorine, although I can't understand why it does not prove under Frama-C Sulfur. Might need additional checks.

-Issue History
Date Modified Username Field Change
2018-06-23 18:47 namin New Issue
2018-06-23 18:47 namin Status new => assigned
2018-06-23 18:47 namin Assigned To => correnson
2018-06-25 09:45 correnson Note Added: 0006565
2018-11-30 10:40 signoles Status assigned => closed
2018-11-30 10:40 signoles Resolution open => fixed
2018-11-30 10:40 signoles Fixed in Version => Frama-C 17-Chlorine
+Issue History