Main Content

-no-assumption-on-absolute-addresses

Remove assumption that absolute address usage is valid

Syntax

-no-assumption-on-absolute-addresses

Description

This option affects a Code Prover analysis only.

-no-assumption-on-absolute-addresses removes the default assumption that absolute addresses used in your code are valid. If you use this option, the verification produces an orange Absolute address usage check when you assign an absolute address to a pointer. Otherwise, the check is green by default.

The type of the pointer to which you assign the address determines the initial value stored in the address. For instance, if you assign the address to an int* pointer, following this check, the verification assumes that the memory zone that the address points to is initialized with an int value. The value can be anything allowed for the data type int.

If you are running an analysis from the user interface (Polyspace® desktop products only), on the Configuration pane, you can enter this option in the Other field. See Other.

Examples

The use of option -no-assumption-on-absolute-addresses can increase the number of orange checks in your code. For instance, the following table shows an additional orange check with the option enabled.

Absolute Address Usage GreenAbsolute Address Usage Orange
void main() {
    int *p = (int *)0x32;
    int x;
    x=*p;
}

In this example, the software produces:

  • A green Absolute address usage check when the address 0x32 is assigned to a pointer p.

  • A green Illegally dereferenced pointer check when the pointer p is read.

    x potentially has all values allowed for an int variable.

void main() {
    int *p = (int *)0x32;
    int x;
    x=*p;
}

In this example, the software produces:

  • An orange Absolute address usage check when the address 0x32 is assigned to a pointer p.

  • A green Illegally dereferenced pointer check when the pointer p is read.

    x potentially has all values allowed for an int variable.

For best use of the Absolute address usage check, leave this check green by default during initial stages of development. During integration stage, use the option -no-assumption-on-absolute-addresses and detect all uses of absolute memory addresses. Browse through them and make sure that the addresses are valid.

Version History

Introduced in R2016a

See Also

Topics