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] Windows header files

Just for the sake of completeness, here are some details about Frama-C's 
support of MSVC headers:

- For the specific version of MSVC mentioned in __fc_machdep.h, we were 
able to incorporate MSVC's includes (Visual Studio's and Microsoft's SDK 
7 directories) without having to use '-no-frama-c-stdlib', which allowed 
us to keep the specifications from our C99's standard library functions, 
and to use GCC's preprocessor, but in Frama-C's MSVC compatibility mode 
(which adds support for a few features). However, this required some 
patches to MSVC's headers, to improve C99 compatibility;

- SAL annotations were not present in the code (the files did not 
include 'sourceanalysis.h', neither directly nor indirectly), neither 
were MSVC-specific types, such as variant types;

- A few parts of the target code had to be patched, notably the use of 
__try/__leave and similar non-standard constructs.

Overall, experience indicates that, if possible, trying to make MSVC's 
headers as "POSIX-like" as possible leads to better results than 
preprocessing everything beforehand using CL.exe. This also results in 
improved standards-compliance and portability for the target code.


On 09/08/18 08:45, Virgile Prevosto wrote:
> Hello,
>
> 2018-08-09 0:42 GMT+02:00 Christine Cunningham 
> <chcunningham5 at gmail.com <mailto:chcunningham5 at gmail.com>>:
>
>     Hi,
>
>     I am using frama-c on windows with cygwin and am trying to run a
>     program that includes windows header files. The
>     share/libc/__fc_machdep.h file seems to imply Visual Studio 2010
>     SP1 (build 160040219) is supported and the user guide section 5.1
>     includes an example of using cl.exe
>
>     frama-c -machdep msvc_x86_64 -verbose 2 -no-cpp-frama-c-compliant
>     -no-frama-c-stdlib -kernel-msg-key pp -cpp-command "cl.exe /c /E
>     %1 > %2" windows.c windows.i
>     [kernel] computing the AST
>     [kernel] parsing
>     [kernel:pp]
>       preprocessing with "cl.exe /c /E %1 > %2 -D__FRAMAC__ -m64
>     windows.c"
>     [kernel] Parsing windows.c (with preprocessing)
>     Microsoft (R) C/C++ Optimizing Compiler Version 16.00.40219.01 for x64
>     Copyright (C) Microsoft Corporation.  All rights reserved.
>
>     cl : Command line warning D9002 : ignoring unknown option '-m64'
>     windows.c
>     [kernel] Parsing C:\cygwin64\tmp\windows.ce3b120.i to Cabs
>     [kernel] Parsing C:\cygwin64\tmp\windows.ce3b120.i
>     [kernel] c://program files (x86)//microsoft visual studio
>     10.0//vc//include//codeanalysis//sourceannotations.h:74:
>       syntax error:
>       Location: between lines 74 and 79, before or at token: [
>       72    };
>       73
>
>       74    typedef enum SA( AccessType ) SA( AccessType );
>       75
>       76    #ifndef SAL_NO_ATTRIBUTE_DECLARATIONS
>       77
>       78    REPEATABLE
>       79    [source_annotation_attribute( SA( Parameter ) )]
>
>       80    struct PreAttribute
>       81    {
>     [kernel] Frama-C aborted: invalid user input.
>
>     Does frama-c not have parsing support for sal annotations?
>
>
> Indeed, Frama-C mostly targets standard ISO C, with a few common 
> extensions, and a bias towards GNU/Linux compatibility. SAL 
> annotations are Microsoft-specific, and based on the example above do 
> not look like "normal" C code at all. Maybe the macro 
> SAL_NO_ATTRIBUTE_DECLARATIONS might be used to obtain a more 
> standard-friendly version (e.g. as attribute and/or macros) that would 
> at least lead to a parseable code in which the annotation would get 
> ignored. Full support for such annotations (in the form of generation 
> of corresponding ACSL annotation) would probably be feasible, but with 
> a non-negligible amount of development.
>
> Best regards,
> -- 
> E tutto per oggi, a la prossima volta
> Virgile
>
>
> _______________________________________________
> 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/20180809/0cc65d5e/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/20180809/0cc65d5e/attachment-0001.bin>