--- layout: fc_discuss_archives title: Message 2 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



Hello,

2018-08-09 0:42 GMT+02:00 Christine Cunningham <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
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180809/89d95507/attachment.html>