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



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>