Hi Jyothi-
There are 2 different conflicting configuration settings happening here:
- 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.
- 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?
