`strlen` used from code makes it no longer possible to prove `assigns \nothing`.
ID0002380: This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002380 | Frama-C | Plug-in > wp | public | 2018-06-23 | 2018-11-30 |
| Reporter | namin | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | Frama-C 17-Chlorine |
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)