用frama-c分析openmp代码

Question

我是新来的。我尝试使用openmp指令在以下c代码上运行值分析插件：

static void kernel_2mm(int ni, int nj, int nk, int nl, float alpha,
    float beta, float *tmp, float *A, float *B, float *C, float *D) {
int i, j, k;
/* D := alpha*A*B*C + beta*D */
#pragma omp parallel for collapse(2) 
for (i = 0; i < ni; i++)
    for (j = 0; j < nj; j++) {
        tmp[i * nj + j] = 0.0;
        for (k = 0; k < nk; ++k)
            tmp[i * nj + j] += alpha * A[i * nk + k] * B[k * nj + j];
    }
#pragma omp parallel for collapse(2) 
for (i = 0; i < ni; i++)
    for (j = 0; j < nl; j++) {
        D[i * nl + j] *= beta;
        for (k = 0; k < nj; ++k)
            D[i * nl + j] += tmp[i * nj + k] * C[k * nl + j];
    }

}

但我犯了以下错误：

rouki@rouki-VirtualBox:~/Téléchargements/frama-c$ frama-c -val  2mm_mp.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i
    (no preprocessing)
[kernel] Parsing 2mm_mp.c (with preprocessing)
[kernel] syntax error at 2mm_mp.c:78:
    76      int i, j, k;
    77      /* D := alpha*A*B*C + beta*D */
    78      #pragma omp parallel for collapse(2) 
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    79        for (i = 0; i < ni; i++)
    80          for (j = 0; j < nj; j++) {
[kernel] Frama-C aborted: invalid user input.

当我尝试将-fopenmp标志添加到preprocesseur选项时，使用：

frama-c -machdep gcc_x86_64 -val -cpp-command 'gcc -fopenmp -C -E -I. ' 2mm_mp.c 

我收到另一条错误消息：

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i
    (no preprocessing)
[kernel] warning: your preprocessor is not known to handle option `-nostdinc'.
    If pre-processing fails because of it, please add
    -no-cpp-frama-c-compliant option to Frama-C's command-line.
    If you do not want to see this warning again, explicitly use option
    -cpp-frama-c-compliant.
[kernel] warning: your preprocessor is not known to handle option `-dD'.
    If pre-processing fails because of it, please add -no-cpp-frama-c-compliant
    option to Frama-C's command-line.
    If you do not want to see this warning again, explicitly use option
    -cpp-frama-c-compliant. 
[kernel] Parsing 2mm_mp.c (with preprocessing)
[kernel] warning: trying to preprocess annotation with an
    unknown preprocessor. 
[kernel] syntax error at 2mm_mp.c:78:
    76      int i, j, k;
    77      /* D := alpha*A*B*C + beta*D */
    78      #pragma omp parallel for collapse(2) 
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    79        for (i = 0; i < ni; i++)
    80          for (j = 0; j < nj; j++) {
[kernel] Frama-C aborted: invalid user input.

如何使frama能够分析代码的openmp？

有没有办法强迫frama使用比gcc (例如: clang，pgcc)更多的编译器？

我使用frama磷-20170501版本，与gcc (Ubuntu5.4.0-6 ubuntu1~16.04.5)。

Answer 1

回答第一个问题(如何使Frama能够使用openmp分析代码？)

OpenMP语用目前(包括Frama-C16硫磺)不受Frama支持。

Frama试图解析它遇到的语用，在某些情况下它只是忽略它们，但在另一些情况下(就像您遇到的那样)，它将尝试解析它们并失败。这样的语用不是C标准的一部分，而是由实现定义的编译器扩展组成的。一些语用，比如#pragma pack()，是由Frama逐个案例支持的.

还请注意，如果可以使用-cpp-command，则不再推荐使用-cpp-extra-args。在您的例子中，使用这意味着使用-cpp-extra-args="-fopenmp"。这并不是说它在这里会有很大帮助，因为这些实用程序无论如何都不受支持，但它应该避免您提到的额外警告。

我担心，目前最好的解决方案是手动注释掉这样的语用，然后再尝试解析源。

回答第二个问题(有没有办法强迫frama使用比gcc (例如: clang，pgcc)更多的编译器？)

是的，像你一样使用-cpp-command确实是做这件事的方法。但是，很好地理解C编译链在这里是有帮助的。特别是，处理某些特定于体系结构的问题(如自定义stdlib报头和非标准特性)的一种通常建议的方法是使用编译器生成预处理代码(例如，gcc -E <inputs> -o file.i)，然后将该文件交给Frama。

请注意，特别是在OpenMP的情况下，GCC使用的语用不会被预处理所删除(这是合乎逻辑的，因为在编译过程中，它在预处理之后使用这些语用)，所以在您的情况下它不会有帮助。但是它确实有帮助，例如，当使用特定于MSVC的代码时，它包含来自Microsoft的几个与GNU libc不兼容的stdlib头)。

最后，请记住，Frama只使用gcc (或另一个编译器)对源代码进行预处理，而不使用编译链的其余部分。因此，GCC和Clang的转换通常不会改变结果，因为两者在预处理方面都实现了非常相似的特性。同样，通常可以只使用-cpp-extra-args而不是-cpp-command，这主要是在-cpp-extra-args还不存在的时候推荐的。