E-ACSL: internal error: raised at file "src/libraries/project/project.ml", line 402
ID0002386: This issue was created automatically from Mantis Issue 2386. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002386 | Frama-C | Plug-in > E-ACSL | public | 2018-07-06 | 2018-11-30 |
| Reporter | evdenis | Assigned To | fmaurica | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | Frama-C 18-Argon | Fixed in Version | Frama-C 18-Argon |
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;
}