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

  • Subject: [Frama-c-discuss] Windows header files
  • From: chcunningham5 at gmail.com (Christine Cunningham)
  • Date: Wed, 8 Aug 2018 18:42:54 -0400
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>