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

Good remark. The post did not mention the usage of `-kernel-msg-key pp` 
to obtain the command given to the preprocessor, and then usage of 
something like GCC's -M to obtain the list of included files during 
preprocessing. Using these, you should hopefully be able to obtain some 
more information.

The Frama-C GUI cannot help here since the AST is not constructed yet, 
so you have to rely mostly on your compiler's options to diagnose and 
fix issues. Still, having the exact command line used by Frama-C is 
essential, so I added a section to the blog post mentioning it.

On 12/07/18 08:04, Divya Muthukumaran wrote:
> Thanks very much Andre. Your reply and the blog post were very 
> helpful, and after getting past those initial errors I am able to make 
> more progress.
> But I am running into this error below-- a bit strange because the the 
> frama-c libc definition of struct tcp_info has that field it is 
> complaining about.
>
> /data/.opam/system/share/frama-c/libc/netinet/tcp.h:u_int32_t*tcpi_rttvar*;
>
>
> Unless that definition is being picked up for somewhere else -- is 
> there any way I can figure out where it is reading that definition from?
>
> --------------------------------------------------------------------------------
>
> [kernel:pp]
>
> preprocessing with "gcc -E -C 
> -I.-I/data/.opam/system/share/frama-c/libc -D__FRAMAC__ 
> -D__FC_MACHDEP_X86_64 -D__USE_GNU 
> -I/data/open-source-case-studies/nginx-1.9.14/ext_headers 
> -I/data/nginx-1.9.14/src/http -I/data/nginx-1.9.14/src/http/modules 
> -I/data/nginx-1.9.14/src/mail -I/data/nginx-1.9.14/src/stream 
> -I/data/nginx-1.9.14/objs -I/data/nginx-1.9.14/src/os/unix 
> -I/data/nginx-1.9.14/src/core -I/data/nginx-1.9.14/src/event -include 
> __fc_stubs.h -dD -nostdinc -m64 src/http/ngx_http_variables.c"
>
> [kernel] Parsing src/http/ngx_http_variables.c (with preprocessing)
>
> [kernel] Parsing /tmp/ngx_http_variables.ca1c446.ibcf80c.pp to Cabs
>
> [kernel] Parsing /tmp/ngx_http_variables.ca1c446.ibcf80c.pp
>
> [kernel] Converting /tmp/ngx_http_variables.ca1c446.ibcf80c.pp from 
> Cabs to CIL
>
> [kernel] src/http/ngx_http_variables.c:1045: User Error:
>
> Cannot find field tcpi_rttvar in type struct tcp_info
>
> 1043
>
> 1044case 1:
>
> 1045value = ti.tcpi_rttvar;
>
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>
> 1046break;
>
> 1047
>
> [kernel] User Error: stopping on file "src/http/ngx_http_variables.c" 
> that has errors.
>
>
>
> Thanks,
> Divya
>
> On Fri, Jul 6, 2018 at 7:26 PM, Andre Maroneze 
> <Andre.OLIVEIRAMARONEZE at cea.fr <mailto:Andre.OLIVEIRAMARONEZE at cea.fr>> 
> wrote:
>
>     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
>     <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
>>     <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
>>     <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>>     https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>>     <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
>
>     -- 
>     André Maroneze
>     Researcher/Engineer CEA/LIST
>     Software Reliability and Security Laboratory
>
>
>     _______________________________________________
>     Frama-c-discuss mailing list
>     Frama-c-discuss at lists.gforge.inria.fr
>     <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>     https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>     <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
>
>
>
>
> _______________________________________________
> 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/20180717/09b919e7/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/20180717/09b919e7/attachment-0001.bin>