--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on August 2018 ---
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 -cpp-command 'CL.exe /C /E %1 > %2' file1.c file2.i I am testing a simple c program #include <windows.h> #include <stdio.h> int main(){ printf("Sleeping\n"); Sleep(10); printf("Done sleeping\n"); return 0; } And am getting an error 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? Does anyone have any suggestions? Thanks, Christine -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180808/f503bfaa/attachment.html>