Search code examples
cframa-cacsl

Frama-C/E-ACSL Error including header files with wrapper script

I am trying to analyze my code using the E-ACSL wrapper script but am facing issues when trying to include header files. For demonstration, I am using the following code and an include directory with one header file.

doubly_linked.c

#include<stdio.h>
#include<stdlib.h>
#include "doubly.h"

struct Node* head; 
struct Node* GetNewNode(int x) {
    struct Node* newNode = (struct Node*)malloc(sizeof(struct Node));
    newNode->data = x;
    newNode->prev = NULL;
    newNode->next = NULL;
    return newNode;
}

void InsertAtTail(int x) {
    struct Node* temp = head;
    struct Node* newNode = GetNewNode(x);
    if(head == NULL) {
        head = newNode;
        return;
    }
    while(temp->next != NULL) temp = temp->next;
    temp->next = newNode;
    newNode->prev = temp;
}

void Print() {
    struct Node* temp = head;
    printf("Forward: ");
    while(temp != NULL) {
        printf("%d ",temp->data);
        temp = temp->next;
    }
    printf("\n");
}

int main() {
    InsertAtTail(2); Print();
}

include/doubly.h

struct Node  {
    int data;
    struct Node* next;
    struct Node* prev;
};

I am running e-acsl-gcc.sh -E "-Iinclude/" doubly_linked.c -c to test this file but am running into the following error

+ /root/.opam/default/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64  -Iinclude/ -no-frama-c-stdlib doubly_linked.c -e-acsl -e-acsl-share=/root/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode a.out.frama.c
[kernel] Parsing doubly_linked.c (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:171: Warning:
  unnamed fields are a C11 extension (use -c11 to avoid this warning)
[variadic] Warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
[variadic] Warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body doubly_linked.c -o a.out
doubly_linked.c:4:10: fatal error: doubly.h: No such file or directory
 #include "doubly.h"
          ^~~~~~~~~~
compilation terminated.

The header files seem to be recognized by the kernel but not E-ACSL.

I am using Frama-C 24.0 (Chromium). Any help would be appreciated. Thanks.

Solution

  • The -c option (compile instrumented code) adds an extra pass to e-acsl-gcc.sh which requires, in your case, an additional option:

      -e         pass additional options to the prepreprocessor
             (e.g. -e "-DPI=3.14 -DE_ACSL_DEBUG_ASSERT")

    When combined with the -E -Iinclude option used to let Frama-C parse the code, this option will let gcc parse the code afterwards. So your command line needs to be:

    e-acsl-gcc.sh -E "-Iinclude" -e "-Iinclude" doubly_linked.c -c

    Note that, if the arguments passed to -E were systematically copied to -e by the script, that could lead to some situations where things would not work. So this duplication is necessary, even if unfortunate.

    On a side note, running the instrumented code from your example in my machine leads to non-deterministic segmentation faults; if I use a more recent Frama-C (25 instead of 24), I get a message explaining this:

    Unsupported TLS area in the middle of heap area.
Example bss TLS address: 0x7f62-9a9e-d750
Example data TLS address: 0x7f62-9a9e-d748
Range of safe locations data: [0x7f62-9a7f-8aa0, 0x7f62-9a9e-d6c8]
Estimated bounds of heap area: [0x7f62-82c5-d11c, 0x7f62-9a96-3f37]
Minimal TLS address: 0x7f62-9a7f-8aa0

    Currently, it is a known issue that, for some architectures with some versions of GCC, this happens (related to undocumented features used in E-ACSL's shadow memory implementation). This is unrelated to your question about e-acsl-gcc.sh, but I'd like to warn you nevertheless. In my case, using gdb makes the crash go away (which also prevents me from debugging it).