Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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