DRS File Polyspace with unknown struct of pointer

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).

Answer 1

[Anirban]

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;
}

.h file named file.h (in same folder as .c file, or folder path provided with option -I):

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:

[Christian]

Thank you for your answer. I think your suggestion is the right direction, but I need something more common.

Here is a shot example. What I want is to tell Polyspace, that the define TEST is in a range of 1…10 so that I will not get an div by zero warning.

H-File:

1.h:

typedef struct myStruct_tag

{

FLOAT a;

} myStruct_type;

extern myStruct_type *my;

#define TEST my->a

C-Files:

1.c:

#include “1.h”

Func()

{

If(100/TEST > 5)

{

}

}

2.c:

Func2()

{

If(1000/TEST > 1)

{

}

}

[Anirban]

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:

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.

Answer 2

[Christian]

Any suggestion to my Comment?