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

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>