Frama-C/E-ACSL错误，包括带有包装器脚本的头文件

Question

我试图使用header包装脚本来分析我的代码，但是当我试图包含头文件时，我会遇到一些问题。为了演示，我使用了下面的代码和一个包含一个头文件的目录。

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;
};

我正在运行e-acsl-gcc.sh -E "-Iinclude/" doubly_linked.c -c来测试这个文件，但是遇到了以下错误

+ /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.

头文件似乎被内核识别，而不是E.

我使用Frama-C24.0(铬).任何帮助都将不胜感激。谢谢。

Answer 1

-c选项(编译工具化代码)为e-acsl-gcc.sh添加了额外的pass，在您的示例中，它需要一个额外的选项：

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

当与用于让Frama解析代码的-E -Iinclude选项相结合时，该选项将允许gcc随后解析代码。因此，您的命令行需要：

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

请注意，如果传递给-E的参数被脚本系统地复制到-e中，则可能导致某些情况下无法工作。因此，这种重复是必要的，即使是不幸的。

另外，在我的机器中运行示例中的检测代码会导致不确定的分段错误；如果我使用最新的Frama-C (25而不是24)，我会收到一条解释如下信息的消息：

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

目前，一个众所周知的问题是，对于某些版本的GCC的体系结构来说，会发生这种情况(与shadow的影子内存实现中使用的无文档特性有关)。这与您关于e-acsl-gcc.sh的问题无关，但我还是要警告您。在我的例子中，使用gdb使崩溃消失(这也阻止了我调试它)。