CODEWITHSUNDEEP
frama-cprogram-slicing
pengwinsurf
pengwinsurf

Reputation: 103

Using Frama-C to slice from a large project

I am trying to experiment with Frama-C against a large code base.

I am using GnuTLS as a target project and directing Frama-C to slice from a source file in this project according to a specific statement.

I used the following command

frama-c -eva -slicing-verbose 8 -no-cpp-frama-c-compliant -cpp-command `gcc ...` -kernel-warn-key annot-error=active -slice-calls some_call_in_a_function file.c

When I run this command I get the following error:

[kernel:annot-error] FRAMAC_SHARE/libc/sys/uio.h:57: Warning:
  unbound logic variable __FC_MAX_OPEN_FILES. Ignoring specification of function writev
[kernel] FRAMAC_SHARE/libc/sys/socket.h:290: User Error:
  Cannot resolve variable __FC_MAX_OPEN_SOCKETS
  288   struct __fc_sockfds_type { int x; };
  289   #endif
  290   //@ ghost struct __fc_sockfds_type __fc_sockfds[__FC_MAX_OPEN_SOCKETS];
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  291
  292   /* Represents the creation of new file descriptors for sockets. */
[kernel] Frama-C aborted: invalid user input.

Does anyone know what's going on here ?

Upvotes: 1

Views: 150

Answers (0)

Related Questions