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