![](https://www.mathworks.com/matlabcentral/answers/uploaded_files/1229882/image.png)
DRS File Polyspace with unknown struct of pointer
2 次查看(过去 30 天)
显示 更早的评论
Hello,
i use pointer that are specified in an struct that are not within the analyses of polyspace. What Polyspace gets is the name of the pointer. So polyspace assumes full range. Is is possible with the DRS file to specify such case? (main function is not a solution)
If I do it like e. g.
structname.variable 5 10 permanent
structname->variable 5 10 permanent
polyspace tells me that it does not know the struct (that's true, but i am not able to change that).
0 个评论
回答(2 个)
Anirban
2022-12-13
编辑:Anirban
2022-12-13
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:
![](https://www.mathworks.com/matlabcentral/answers/uploaded_files/1229882/image.png)
2 个评论
Anirban
2022-12-16
编辑:Anirban
2022-12-16
Yes, you can specify this constraint exactly like the example I showed earlier.
I tried with this code:
Source file:
#include "myfile.h"
int Func()
{
if(100/TEST) {
}
return TEST;
}
Header file (myfile.h):
typedef struct myStruct_tag
{
float a;
} myStruct_type;
extern myStruct_type *my;
#define TEST my->a
Here is the constraint (DRS) I specified in the Polyspace user interface:
![](https://www.mathworks.com/matlabcentral/answers/uploaded_files/1233597/image.png)
If you run Code Prover, you will see a green division by zero. The tooltip on the division operation will show you that the DRS is being applied as expected.
Note: When generating a DRS in the Polyspace user interface, make sure that the Source code language is set to C. If the language is CPP or C-CPP, structures are treated in the same category as C++ classes and the ability to specify DRS becomes quite limited.
另请参阅
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!