In Polyspace Code, while configuring DRS, even if a user defined function's argument is initialized with "Init Range", it is not affective in verification

if true
  Func1(arg1, arg2, arg3)
{
....
....
local variable = arg1 + arg2;
 if (arg3>=200)
 {
  /*do something/no unreachable code*/
 }
}
main()
{
...
Func1(10,20,100);

}

end

During DRS configuration, arg3 is initialised to 200. Project is configured to be Verified at whole application level.

But arg3 is not taking 200 during verification.In check details/tip pointing, it is considering only 100.

Request : Inorder to test my Protection code(cases where error flag check), please provide a solution

Answer 1

[Matt Rhodes]

Hi Jyothi-

There are 2 different conflicting configuration settings happening here:

1. The DRS configuration, also known as Constraint Specification, is used with the main generator to tell the main generator how to constrain calls to functions.
2. The option to "Verify Whole Application" means that Polyspace is expecting you to provide a main() for the analysis, which you are doing.

In other words, you have to tell Polyspace to "Verify Module or Library" instead of "Verify Whole Application." I also see that you are providing a main in your example code. When you do this, Polyspace sees the main you provide and overrides your setting to be "Verify Whole Application" because it cannot correctly resolve which main to use on its own. You will have to either exclude the main you are providing, or use a MACRO to rename main so that Polyspace can use its own main generator.

One more thought. If you are using your main, and you are seeing the argument being initialized with 100 instead of 200, that is because your main is causing the initialization to 100. If you are actually using 100 instead of 200, what is the reason you are trying to get Polyspace to initialize this value to 200?