--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Casting to a generic function pointer



Yes, it is related to using preprocessed files. Your preprocessed file 
must have included your system's headers, which do not include Frama-C's 
ACSL specifications for functions such as strlen(). As such, when 
Frama-C parses the .i files, it finds just a prototype without any 
specifications, and it will not assume that the function called strlen() 
in /your/ file is necessarily the one from <string.h>.

One solution might be to rename the .i file as a .c (to ensure Frama-C 
will preprocess it), manually add "#include <string.h>" and similar 
files, and try to parse it again. However, this is likely to create 
conflicts between the types in your prototypes with the ones in 
Frama-C's libc. You may have to erase some declarations from your 
preprocessed file.

The overall question of parsing such code bases is interesting and will 
be the subject of a future post in the Frama-C blog.

The summarized version is that the reason why `cpu_set_t` is not known 
is because it is not POSIX, and thus not present in Frama-C's libc. You 
should manually add such a typedef or macro to define it, probably based 
on the type used in your system. Something similar to this should work:

typedef unsigned long __cpu_mask;

# define __NCPUBITS (8 * sizeof (__cpu_mask))
# define CPU_SETSIZE 1024

typedef struct {
   __cpu_mask __bits[CPU_SETSIZE / __NCPUBITS];
} cpu_set_t;

These definitions are based on those found in my system's libc.

To parse nginx, you will likely need to include other types and 
definitions in a similar way. In the end, this step may take a 
significant amount of time, which is one of the reasons that the 
open-source-case-studies repository 
(https://github.com/Frama-C/open-source-case-studies) exists: so that 
only one person will ever have to work through this parsing stage, 
allowing others to proceed from there.

As a final note: it is helpful, when possible, to disable optional, 
non-portable features from ./configure scripts, either with options such 
as --without-<feature>, or by manually editing the generated config.h 
file (e.g. objs/ngx_auto_config.h), and setting HAVE_<FEATURE> macros to 0.



On 04/07/18 23:17, Divya Muthukumaran wrote:
> Thanks for the detailed answer Andre. I'm not sure if it has something 
> to do with the fact that I am running this on preprocessed *.i files.
> I tried to run them on the original *.c files, but that fails with:
>
> [kernel] /data/nginx-1.9.14/src/os/unix/ngx_setaffinity.h:16:
>   syntax error:
>   Location: line 16, between columns 8 and 18, before or at token: 
> ngx_cpuset_t
>   14    #if (NGX_HAVE_SCHED_SETAFFINITY)
>   15
>   16    typedef cpu_set_t ngx_cpuset_t;
>         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>   17
>   18    #elif (NGX_HAVE_CPUSET_SETAFFINITY)
>
> I did try frama-c on a toy example with the strlen and malloc calls 
> and that works perfectly.

-- 
André Maroneze
Researcher/Engineer CEA/LIST
Software Reliability and Security Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180705/1036dad2/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180705/1036dad2/attachment.bin>