Issue in parsing __declspec( dllimport) in C++ code

[jkumarss]

Hi - Here are the 2 issues i'm facing.

1. I have tried the following example with an open source CBMC (latest one). It throws a parser error while parsing the function func() although I have installed visual studio 2010 professional. Can someone help here?
   #define DllImport __declspec( dllimport)
   DllImport void func();

2. I'm not able to include the standard directory using #include<stdio.h>. Rather the tool works with #include "stdio.h"

Request if someone could help me here.

Thanks
Jay

[thomasspriggs]

1. This seems to be fixed in the current develop version of cbmc.

Example tried -

declspec.c

#define DllImport __declspec( dllimport)
DllImport void func();

void main()
{
}

cbmc output

$ cbmc ./declspec.c 
CBMC version 5.25.0 (cbmc-5.25.0-dirty) 64-bit x86_64 linux
Parsing ./declspec.c
Converting
Type-checking declspec
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000440711s
size of program expression: 38 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 9.806e-06s
VERIFICATION SUCCESSFUL

2. Pre-processor actions such as include are dealt with using your compiler rather than by cbmc. So there is probably something not right with the environment variables for your include path.

I am going to close this out. Given the length of time since you asked your questions, my answers are probably irrelevant. However if you need more help with your includes, feel free to reopen.