Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002386Frama-CPlug-in > E-ACSLpublic2018-07-06 10:442018-07-12 09:11
Reporterevdenis 
Assigned Tofmaurica 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002386: E-ACSL: internal error: raised at file "src/libraries/project/project.ml", line 402
DescriptionError:
$ 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;
}
TagsNo tags attached.
Attached Filesc file icon memchr.c [^] (1,236 bytes) 2018-07-06 10:44 [Show Content]
c file icon memchr_v2.c [^] (1,228 bytes) 2018-07-12 07:53 [Show Content]

- Relationships

-  Notes
(0006583)
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
(0006587)
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
(0006588)
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.

- Issue History
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker