c - Frama-c [内核] 用户错误 : Length of array is zero. 不支持此扩展

Question

我正在尝试使用此命令生成 c 程序的 PDG

frama-c -machdep x86_64 -pdg -cpp-command 'gcc -C -E -std=c99 -I. ' try.c

但我得到以下错误

[kernel] preprocessing with "gcc -C -E -std=c99 -I.   try.c"

/usr/include/x86_64-linux-gnu/bits/byteswap.h:47:[kernel] warning: Calling undeclared function __builtin_bswap32. Old style K&R code?

/usr/include/x86_64-linux-gnu/bits/byteswap.h:111:[kernel] warning: Calling undeclared function __builtin_bswap64. Old style K&R code?

/usr/include/x86_64-linux-gnu/bits/fcntl-linux.h:316:[kernel] user error: Length of array is zero. This extension is unsupported

[kernel] user error: skipping file "try.c" that has errors.

[kernel] Frama-C aborted: invalid user input.

我该如何解决这个问题？ 更新: C代码是

#include<stdio.h>
int main()
{
    int n,m;
    int i,j;
    int flag=1;

    scanf("%d%d",&n,&m);

    int a[n][m];

    for(i=0;i<n;i++)
    {
        for(j=0;j<m;j++)
        {
            scanf("%d",&a[i][j]);
        }
    }

    for(i=0;i<n-1;i++)
    {
        if(a[i][0]==a[i+1][0])
        {
            flag=0;
            break;
        }

        for(j=0;j<m-1;j++)
        {
                if(a[i][j]!=a[i][j])
                {
                    flag=0;
                    break;
                }
        }
        if(flag==1)
        {
            continue;
        }

        else
            break;
    }

    if(flag==1)
        printf("YES");
    else
        printf("NO");

    return 0;
}

使用的frama-c版本是

Version: Fluorine-20130601 Compilation date: Mon Dec 23 22:50:26 UTC 2013

Share path: /usr/share/frama-c (may be overridden with FRAMAC_SHARE variable)

Library path: /usr/lib/frama-c (may be overridden with FRAMAC_LIB variable)

Plug-in paths: /usr/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)

Answer 1

自 Frama-C Aluminium(2016 年 5 月发布)以来支持零长度数组。这是更新日志的相关摘录:

 -! Cil       [2015/12/02] Changes in the handling of incomplete structs and
              zero-length arrays. Initialization of incomplete (completely
              undefined) structs is now duly rejected. Several compiler
              extensions to the C99 standard (empty initializers,
              zero-length arrays, etc.) now require a GCC or MSVC machdep
              (e.g. -machdep gcc_x86_32).

如前所述，您应该使用 GCC machdep，在您的情况下即 gcc_x86_64。