CODEWITHSUNDEEP
cframa-c
Perseus14
Perseus14

Reputation: 487

Frama-c [kernel] user error: Length of array is zero. This extension is unsupported

I am trying to generate PDG of a c program using this command 

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

but I get this following error

[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.

How do I solve this? Update: The C code is 

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

The version of frama-c used is

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)

Upvotes: 1

Views: 114

Answers (1)

byako
byako

Reputation: 3422

Zero-length arrays are supported since Frama-C Aluminium (released in may 2016). This is the relevant excerpt from the Changelog:

 -! 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).

As indicated, you should use a GCC machdep, namely gcc_x86_64 in your case.

Upvotes: 2

Related Questions