View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002386 | Frama-C | Plug-in > E-ACSL | public | 2018-07-06 10:44 | 2018-11-30 10:07 | ||||
Reporter | evdenis | ||||||||
Assigned To | fmaurica | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Frama-C 18-Argon | Fixed in Version | Frama-C 18-Argon | ||||||
Summary | 0002386: E-ACSL: internal error: raised at file "src/libraries/project/project.ml", line 402 | ||||||||
Description | Error:$ frama-с -version Chlorine-20180501 $ frama-с -e-acsl memchr.c ... [e-acsl] test.c:21: Warning: E-ACSL construct `variant' is not yet supported. Ignoring annotation. [e-acsl] test.c:27: Warning: invalid E-ACSL construct `non integer variable k in quantification ∀ u8 *k; (u8 *)s ≤ k < p ⇒ *k ≢ (u8)c'. Ignoring annotation. [kernel] test.c:26: Failure: mkBinOp: p - (unsigned char const *)s == __gen_e_acsl_at - n [kernel] Current source was: test.c:39 The full backtrace is: Raised at file "src/libraries/project/project.ml", line 402, characters 50-57 Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023 Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34 Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22 Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 791, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8 Frama-C aborted: internal error. Example code: /*@ requires \typeof(s) <: \type(u8 *); requires \valid((u8 *)s+(0..n-1)); assigns \nothing; behavior found: assumes \exists u8 *p; (u8 *)s <= p < (u8 *)s + n && *p == (u8) c; ensures s <= \result <= s + n; ensures \forall u8 *p; (u8 *)s <= p < (u8 *)\result ==> *p != (u8) c; ensures *((u8 *)\result) == (u8) c; behavior not_exists: assumes \forall u8 *p; (u8 *)s <= p < (u8 *)s + n ==> *p != (u8) c; ensures \result == \null; complete behaviors; disjoint behaviors; */ void *memchr(const void *s, int c, size_t n) { const unsigned char *p = s; /*@ loop invariant 0 <= n <= \at(n,Pre); loop invariant (u8 *)s <= p <= (u8 *)s + \at(n,Pre); loop invariant p - s == \at(n,Pre) - n; loop invariant \forall u8 *k; (u8 *)s <= k < p ==> *k != (u8) c; loop variant n; */ while (n-- != 0) { if ((unsigned char) c == *p++) { return (void *)(p - 1); } } //@ assert n == (size_t)(-1); return NULL; } int main(int argc, char *argv[]) { const char *s = "1234567890"; void *ptr; ptr = memchr(s, '0', 11); ptr = memchr(s, 'a', 11); ptr = ptr; return 0; } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 2018-07-11 15:56 |
Which E-ACSL version are you using? I tried it with the latest one (Chlorine) and it works fine. $ e-acsl-gcc.sh -c memchr.c $ ./a.out.e-acsl $ echo $? 0 |
evdenis (reporter) 2018-07-12 07:56 |
On the second file, frama-с reports the error. But e-acsl-gcc.sh doesn't crash. $ frama-с -e-acsl memchr_v2.c [kernel] memchr_v2.c:24: Failure: mkBinOp: p - (unsigned char const *)s == __gen_e_acsl_at - n [kernel] Current source was: memchr_v2.c:38 The full backtrace is: Raised at file "src/libraries/project/project.ml", line 402, characters 50-57 Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023 Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34 Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22 Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 791, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8 Frama-C aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Chlorine-20180501. $ e-acsl-gcc.sh -c memchr_v2.c $ ./a.out.e-acsl $ echo $? 0 |
signoles (manager) 2018-07-12 09:07 |
There is indeed a bug in E-ACSL here. However, when using E-ACSL directly from Frama-C, you should specify the machdep wrt your target system, e.g. gcc_x86_64 if you plan to compile the code with gcc on a 64-bit architecture. $ frama-c -machdep gcc_x86_64 -e-acsl memchr_v2 If so, the bug disappears. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2018-07-06 10:44 | evdenis | New Issue | |
2018-07-06 10:44 | evdenis | Status | new => assigned |
2018-07-06 10:44 | evdenis | Assigned To | => signoles |
2018-07-06 10:44 | evdenis | File Added: memchr.c | |
2018-07-11 15:56 | signoles | Note Added: 0006583 | |
2018-07-11 15:56 | signoles | Status | assigned => feedback |
2018-07-12 07:53 | evdenis | File Added: memchr_v2.c | |
2018-07-12 07:56 | evdenis | Note Added: 0006587 | |
2018-07-12 07:56 | evdenis | Status | feedback => assigned |
2018-07-12 09:07 | signoles | Note Added: 0006588 | |
2018-07-12 09:11 | signoles | Assigned To | signoles => fmaurica |
2018-09-05 16:30 | signoles | Target Version | => Frama-C 18-Argon |
2018-10-05 09:17 | signoles | Status | assigned => resolved |
2018-10-05 09:17 | signoles | Resolution | open => fixed |
2018-11-30 10:07 | signoles | Fixed in Version | => Frama-C 18-Argon |
2018-11-30 10:07 | signoles | Status | resolved => closed |