Exponenta Banner
exponenta event banner

Absolute address usage

Указателю назначен абсолютный адрес

развернуть все на странице

Описание

Эта проверка появляется, когда указателю назначается абсолютный адрес.

По умолчанию эта проверка имеет зеленый цвет. Программа принимает следующее относительно абсолютного адреса:

  • Адрес действителен.

  • Тип указателя, которому вы присваиваете адрес, определяет начальное значение, сохраненное в адресе.

    Если вы присвоите адрес int* указатель, зона памяти, на которую указывает адрес, инициализируется int значение. Значение может быть любым допустимым для типа данных int.

Чтобы сделать этот флажок оранжевым по умолчанию для каждого абсолютного использования адреса, используйте опцию командной строки -no-assumption-on-absolute-addresses.

Примеры

расширить все

enum typeList {CHAR,INT,LONG};
enum typeList showType(void);
long int returnLong(void);

void main() {
    int *p = (int *)0x32; //Green absolute address usage
    enum typeList myType = showType();

    char x_char;
    int x_int;
    long int x_long;

    if(myType == CHAR)
        x_char = *p;
    else if(myType == INT)
        x_int = *p;
    else {
        x_long = *p;
        long int x2_long = returnLong();
    }
}

В этом примере опция -no-assumption-on-absolute-addresses не используется. Поэтому проверка Absolute address usage зеленая, когда указатель p присваивается абсолютный адрес.

После этой проверки верификации принимает, что адрес инициализируется int значение. Если вы используете x86_64 для Target processor type (-target) (sizeof(char) < sizeof(int) < sizeof(long int)), предположение приводит к следующему:

  • В if(myType == CHAR) ветвь, оранжевая Overflow происходит из-за x_char невозможно вместить все значения, разрешенные для int переменная.

  • В else if(myType == INT) ветвь, если поместить курсор на x_int в результатах верификации подсказка показывает, что x_int потенциально все значения разрешены для int переменная.

  • В else ветвь, если поместить курсор на x_long, подсказка показывает, что x_long потенциально все значения разрешены для int переменная. Если поместить курсор на x2_long, подсказка показывает, что x2_long потенциально все значения разрешены для long int переменная. Область значений значений, которые x2_long может взять шире, чем значения, разрешенные для int переменная в том же целевом объекте.

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

В этом примере опция -no-assumption-on-absolute-addresses используется. Проверка Absolute address usage оранжевая, когда указатель p присваивается абсолютный адрес.

После этой проверки:

  • Polyspace® считает, что p указывает на допустимое расположение памяти. Поэтому проверка Illegally dereferenced pointer на следующей линии имеет зеленый цвет.

  • В следующих двух линиях указатель p приращение и последующее разыменование. В этом случае проверка Illegally dereferenced pointer появляется в dereference, а не в Absolute address usage проверке, хотя p все еще указывает на абсолютный адрес.

Проверяйте информацию

Группа: Статическая память
Язык: C | C++
Акроним: ABS_ADDR

Документация Polyspace Code Prover

Поддержка