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

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>