--- layout: fc_discuss_archives title: Message 15 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



Just to inform you, the blog post about parsing code bases such as nginx 
is online:

http://blog.frama-c.com/index.php?post/2018/07/06/Parsing-realistic-code-bases-with-Frama-C


On 05/07/18 15:22, Andre Maroneze wrote:
>
> 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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
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/20180706/4e765e94/attachment-0001.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/20180706/4e765e94/attachment-0001.bin>