XML File Format for Polyspace Analysis Constraints

For a more precise Polyspace^® analysis, you can specify constraints on global variables, function inputs and stubbed functions. You can specify the constraints in the user interface of the Polyspace desktop products or at the command line as an XML file. For the general workflow, see Specify External Constraints for Polyspace Analysis.

This topic describes details of the constraint XML file schema. You typically require this information only if you create a constraint XML from scratch. If you run a verification once, the software automatically generates a template constraint file drs-template.xml in your results folder. Instead of creating a constraint XML file from scratch, it is easier to edit this template XML file to specify your constraints. For some examples, see:

For another explanation of what the XML tags mean, see External Constraints for Polyspace Analysis.

You can also see the information in this topic and the underlying XML schema in polyspaceroot\polyspace\drs. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2019a.

Syntax Description — XML Elements

The constraints file contains the following XML elements:

<global> element — Declares the global scope, and is the root element of the XML file.
<file> element — Declares a file scope. Must be enclosed in the <global> element. May enclose any variable or function declaration. Static variables must be enclosed in a file element to avoid conflicts.
<scalar> element— Declares an integer or a floating point variable. May be enclosed in any recognized element, but cannot enclose any element. Sets init/permanent/global asserts on variables.
<pointer> element — Declares a pointer variable. May enclose any other variable declarations (including itself), to define the pointed objects. Specifies what value is written into pointer (NULL or not), how many objects are allocated and how the pointed objects are initialized.
<array> element — Declares an array variable. May enclose any other variable definition (including itself), to define the members of the array.
<struct> element — Declares a structure variable or object (instance of class). May enclose any other variable definition (including itself), to define the fields of the structure.
<function> element — Declares a function or class method scope. May enclose any variable definition, to define the arguments and the return value of the function. Arguments should be named arg1, arg2, …argn and the return value should be called return.

The following notes apply to specific fields in each XML element:

(*) — Fields used only by the GUI. These fields are not mandatory for verification to accept the ranges. The field line contains the line number where the variable is declared in the source code, complete_type contains a string with the complete variable type, and base_type is used by the GUI to compute the min and max values. The field comment is used to add information about any node.
(**) — The field name is mandatory for scope elements <file> and <function> (except for function pointers). For other elements, the name must be specified when declaring a root symbol or a struct field.
(***) — If more than one attribute applies to the variable, the attributes must be separated by a space. Only the static attribute is mandatory, to avoid conflicts between static variables having the same name. An attribute can be defined multiple times without impact.
(****) — This element is used only by the GUI, to determine which init modes are allowed for the current element (according to its type). The value works as a mask, where the following values are added to specify which modes are allowed:
- 1: The mode “NO” is allowed.
- 2 : The mode “INIT” is allowed.
- 4: The mode “PERMANENT” is allowed.
- 8: The mode “MAIN_GENERATOR” is allowed.
For example, the value “10” means that modes “INIT” and “MAIN_GENERATOR” are allowed. To see how this value is computed, refer to Valid Modes and Default Values.
(*****) — A sub-element of a pointer (i.e. a pointed object) will be taken into account only if init_pointed is equal to SINGLE, MULTI, SINGLE_CERTAIN_WRITE or MULTI_CERTAIN_WRITE.
(******) — SINGLE_CERTAIN_WRITE or MULTI_CERTAIN_WRITE are available for parameters and return values of stubbed functions only if they are pointers. If the parameter or return value is a structure and the structure has a pointer field, they are also available for the pointer field.

`<file>` Element

Field	Syntax
`name`	`filepath_or_filename`
`comment`	`string`

`<scalar>` Element

Field	Syntax
`name` (**)	`name`
`line` (*)	`line`
`base_type` (*)	`intx uintx floatx`
`Attributes` (*******)	`volatile extern static const`
`complete_type` (*)	`type`
`init_mode`	`MAIN_GENERATOR IGNORE INIT PERMANENT disabled unsupported`
`init_modes_allowed` (*)	`single value` (********)
`init_range`	`range` `disabled unsupported`
`global_ assert`	`YES NO disabled unsupported`
`assert_range`	`range` `disabled unsupported`
`comment`(*)	`string`

`<pointer>` Element

Field	Syntax
`Name` (**)	`name`
`line` (*)	`line`
`Attributes` (*******)	`volatile extern static const`
`complete_type` (*)	`type`
`init_mode`	`MAIN_GENERATOR IGNORE INIT PERMANENT disabled unsupported`
`init_modes_allowed` (*)	`single value` (********)
`initialize_ pointer`	May be: `NULL Not NULL NULL`
`number_ allocated`	`single value` `disabled unsupported`
`init_pointed` (******)	`MAIN_GENERATOR` `NONE` `SINGLE` `MULTI` `SINGLE_CERTAIN_WRITE` `MULTI_CERTAIN_WRITE` `disabled`
`comment`	`string`

`<array>` and `<struct>` Elements

Field	Syntax
`Name` (**)	`name`
`line` (*)	`line`
`complete_type` (*)	`type`
`attributes` (*******)	`volatile extern static const`
`comment`	`string`

`<function>` Element

Field	Syntax
`Name` (**)	`name`
`line` (*)	`line`
`main_generator_called`	`MAIN_GENERATOR YES NO disabled`
`attributes` (*******)	`static extern unused`
`comment`	`string`

Valid Modes and Default Values

Scope	Type		Init modes	Gassert mode	Initialize pointer	Init allocated	Default
Global variables	Base type	Unqualified/ static/ const scalar	MAIN_ GENERATOR IGNORE INIT	YES NO			Main generator dependent
		Unqualified/ static/ const scalar	PERMANENT	disabled			Main generator dependent
		Volatile scalar	PERMANENT	disabled			PERMANENT min..max
		Extern scalar	INIT	YES NO			INIT min..max
		Extern scalar	PERMANENT	disabled			INIT min..max
	Struct	Struct field	Refer to field type
	Array	Array element	Refer to element type
Global variables	Pointer	Unqualified/ static/ const scalar	MAIN_ GENERATOR IGNORE INIT		May be NULL Not NULL NULL	NONE SINGLE MULTI	Main generator dependent
		Volatile pointer	un- supported		un- supported	un- supported
		Extern pointer	IGNORE INIT		May be NULL Not NULL NULL	NONE SINGLE MULTI	INIT May be NULL max MULTI
		Pointed volatile scalar	un- supported	un- supported
		Pointed extern scalar	INIT	un- supported			INIT min..max
		Pointed other scalars	MAIN_ GENERATOR INIT	un- supported			MAIN_ GENERATOR dependent
		Pointed pointer	MAIN_ GENERATOR INIT/	un- supported	May be NULL Not NULL NULL	NONE SINGLE MULTI	MAIN_ GENERATOR dependent
		Pointed function	un- supported	un- supported
Function parameters	Userdef function	Scalar parameters	MAIN_ GENERATOR INIT	un- supported			INIT min..max
		Pointer parameters	MAIN_ GENERATOR INIT	un- supported	May be NULL Not NULL NULL	NONE SINGLE MULTI	INIT May be NULL max MULTI
		Other parameters	Refer to parameter type
	Stubbed function	Scalar parameter	disabled	un- supported
		Pointer parameters	disabled		disabled	NONE SINGLE MULTI SINGLE_CERTAIN_WRITE MULTI_CERTAIN_WRITE	MULTI
		Pointed parameters	PERMANENT	un- supported			PERMANENT min..max
		Pointed const parameters	disabled	un- supported
Function return	Userdef function	Return	disabled	un- supported	disabled	disabled
	Stubbed function	Scalar return	PERMANENT	un- supported			PERMANENT min..max
	Stubbed function	Pointer return	PERMANENT	un- supported	May be NULL Not NULL NULL	NONE SINGLE MULTI SINGLE_CERTAIN_WRITE MULTI_CERTAIN_WRITE	PERMANENT May be NULL max MULTI