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