If your code compiles, Polyspace should have the struct definition. I am wondering if you have compilation errors. Anyway, your DRS format makes it seem like you are using text files for DRS. Use of text files for DRS is deprecated. Instead, you can use the XML format. The XML format can be easily generated from the Polyspace user interface (there is the additional benefit that if your code does not compile, the XML generation step will fail and you will know the issue right away). See Specify External Constraints for Polyspace Analysis.
Here is an example of using DRS XML to constrain struct pointers. Suppose you have these two files:
.c file:
#include "file.h"
int func(struct myStruct* myStructPtr) {
return myStructPtr->b;
}
struct myStruct{
int a;
int b;
};
To constrain the argument to the function func, you can specify a DRS XML like the following. The XML imposes a range 0..10 on the second field of the structure being pointed to by the pointer myStructPtr.
<?xml version="1.0" encoding="UTF-8"?>
<!--EDRS Version 2.0-->
<global>
<file name="D:\\Polyspace\\R2023a\\MATLAB Answers\\DRS_struct_pointers\\file.c">
<function name="func" line="3" attributes="unused" main_generator_called="MAIN_GENERATOR" comment="">
<pointer name="arg1" line="3" complete_type="struct myStruct *" init_mode="INIT" init_modes_allowed="10" initialize_pointer="Not NULL" number_allocated="1" init_pointed="SINGLE" comment="">
<struct line="3" complete_type="struct myStruct" comment="">
<scalar name="b" line="3" base_type="int32" complete_type="int32" init_mode="INIT" init_modes_allowed="10" init_range="0..10" global_assert="unsupported" assert_range="unsupported" comment=""/>
</struct>
</pointer>
<scalar name="return" line="3" base_type="int32" complete_type="int32" init_mode="disabled" init_range="disabled" global_assert="unsupported" assert_range="unsupported" comment=""/>
</function>
</file>
</global>
The XML looks intimidating, but all that needs to be specified in the Polyspace user interface is this information:
