--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2018 ---
[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>