Frama-c [kernel] user error: Length of array is zero. This extension is unsupported
Frama-c [kernel] user error: Length of array is zero. This extension is unsupported
我正在尝试使用此命令生成 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)
从 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。
我正在尝试使用此命令生成 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)
从 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。