Polyspace Code Prover not able to find windows.h as header file. getting compilation errors because of windows dependencies.

I am using polyspace code prover for doing static analysis, in that my source code contains 'windows.h' as header file like #include<windows.h>, but the Polyspace tool is unable find the file and I mentioned compiler option in the tool as Visual15.x and trarget processor as i386. please provide the solution.

Answer 1

[Anirban]

Hi Venkata,

Specifying the compiler name is not sufficient for Polyspace to locate the include folders. The folder paths vary across installations and operating systems, so it is left to the user to specify them. There is a much better alternative approach to running a Polyspace analysis from a Visual Studio solution. See the bottom of this reply.

First, the manual approach. You have to specifically point to the Visual Studio include folders using the option -I on the command line (or add the include folders to the project in the Polyspace user interface).

You have to locate the include folders in your Visual Studio installation. The typical paths are:

• C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\include\
• C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\atlmfc\include\

But windows.h is not located here. It would be in something like:

C:\Program Files (x86)\Windows Kits\8.1\Include\um

To avoid the problem of having to manually locate and then specify the include folders, Polyspace supports a different approach to create a Polyspace project from a Visual Studio project. You can trace the commands that Visual Studio runs and create the appropriate -I-s to the right include folders. See Create Project Using Visual Studio Information.

[Venkata Narendra]

Thanks for your answer Anirban :)

[Venkata Narendra]

Hi Anirban,

After following the procedure Create Project Using Visual Studio Information. I am facing some compilation errors in Polyspace Code Prover because of visual studio files and windows files.

I selected x86_64 as a target processor you can see in the image.

I am not able to find the issue.

Please help me to resolve the issue.

Let me know, if you need anything further

Thank you

[Anirban]

Hi Venkata,

The idea is that if you generate a project from a Visual Studio solution, the target information will be extracted from the solution itself. After this, you should not have to do anything else. You can run Polyspace and see results.

If you go to Advanced Settings, you should see an option -custom-target that reflects the target settings extracted.

Can you tell me if there is any other change you made besides setting Target Processor Type to x86_64 ? In fact, can you not make any change after project generation and see if you still get the error?

The error message highlighted in your screenshot indicates that line 227 is conflicting with line 226. Line 227 has __readcr0 defined as unsigned long, which is conflicting with line 226, which has __readcr0 defined as unsigned __int64. The message says that the previous declaration is unsigned long long __readcr0. So, __int64 is being interpreted as long long. We have to find out why.

This might be an issue specific to your Visual Studio solution and Support is better at handling specific issues. But before redirecting to Support, we just want to check if you made any other change to the Polyspace project after project generation.

[Venkata Narendra]

Hi Anirban,

Thanks for your answer.

When I generate a project from a Visual Studio solution, the target information extracting is i386, when I run the analysis with this settings I am not getting any issue.

But when I changed the target to x86_64 target I am facing the above mentioned compilation issues.

And I am not doing any other changes in the polyspace configuration.

Actually I need to use Intel 64 bit processor as taget a processor so that is the reason I have changed the target.

How target information will be extracted from the solution?

Is any chance to set the target while creating the project using visual studio information?

And one more thing I want to know is whie creating the project by visual studio solution, what is the use of 'Add advanced configure options'.

Please let me know, if you have any suggestions

Thank you

[Anirban]

Hi Venkata,

The idea behind creating a Polyspace project using a Visual Studio project is that the Polyspace project represents faithfully what you do inside Visual Studio. If you are building for a 64-bit target in Visual Studio, then the Polyspace project is extracting the right settings from your Visual Studio build. The settings probably do not correspond exactly to the x86_64 sizes, but they are what you are using in Visual Studio. Maybe you can use the Visual Studio documentation to make sure that you are building for a 64-bit target? See, for instance, this Visual Studio documentation topic.

(Note that even though the target that appears to be set is i386, the target that is actually used is given in the Advanced Settings node using the option -custom-target. It is a quirk of the user interface. If, in fact, you are building for a 64-bit target in Visual Studio and the i386 is the only reason you think the Visual Studio settings are not used, then you can rest assured. The -custom-target value reflects the real sizes used.)

In your workflow, when you changed the target to x86_64, what happened is the following (I also made some edits to my previous answer to be more precise): when you created a Polyspace project using Visual Studio information, the polyspace-configure command ran underneath to extract the following information:

• Sizes of data types (set in the Polyspace project using -custom-target)
• Macro definitions (set in the Polyspace project using -D).Some of the macro definitions are also related to the target used in Visual Studio.

Now, when you changed the target to x86_64, what you changed was the first thing above but not the second. That led to conflicts like incompatible declarations (most likely because the sizes that correspond to x86_64 do not correspond exactly to the sizes extracted from your Visual Studio build).

The Add advanced configure options are all the advanced options that the polyspace-configure command takes. See the full options list. Typically, you do not need these options. You just specify the build command (or in this case, the Visual IDE executable) and the run with the default options works fine. That is why they were not exposed in the user interface through nice GUI fields.

Answer 2

[Martin Dowie]

While using the installed headers that come with, e.g. VS2019, gets you answer quickly, it often doesn't give you good answer, as Polyspace will use it's "worst-case" assumptions. You may find it more helpful to create you own re-usable stubs in which you can provide more accurate knowledge about the behaviour of functions declared in headers wrt in-out parameters or function return values. This does incur upfront cost to generate but you only need to include what you use, and future projects can re-use what you start, and add anything extra they need.