c - Frama-c [内核]用户错误:数组的长度为零。不支持此扩展

我试图用这个命令生成一个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版本是
版本：氟-20130601编译日期：2013年12月23日星期一22:50:26 UTC
共享路径：usr/Share/frama-c（可以用FRAMAC_Share变量重写）
库路径：usr/lib/frama-c（可以用FRAMAC_lib变量重写）
插件路径/usr/lib/frama-c/plugins（可以用FRAMAC_Plug in变量重写）

最佳答案

自Frama-C Aluminum（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在您的情况下。

关于c - Frama-c [内核]用户错误:数组的长度为零。不支持此扩展，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/47392044/