Exponenta Banner

Absolute address usage

Абсолютный адрес присвоен указателю

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

Описание

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

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

  • Адрес допустим.

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

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

Анализ делает эти предположения относительно абсолютного использования адреса:

  • Проверка не отмечает абсолютные адреса, если они включают переменные или адресную арифметику с указателями. Например, x = *(int*)0x7 адрес рассматривается абсолютным адресом. x = *(int*)(0x7 + y) адрес не является абсолютным адресом, должным его использование переменных.

  • Если вы присваиваете абсолютный адрес указателю, анализ принимает, что резкое местоположение может содержать любое значение, допускал резкий тип данных. Например, следующий ptr = (int*)0x32, анализ принимает тот *ptr может содержать любой int значение. После последовательности бросков, таких как ptr = (int*)(char*)0x32, анализ учитывает только наиболее удаленный бросок, в этом случае, int*.

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

Примеры

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

void func(int offset) {
    int *p = (int *)0x32;             // Green absolute address usage
    int *q = (int *)(0x32+offset);    // No absolute address check happens here
}

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

Эта проверка выполнена только на строгих абсолютных адресах. Как int *q = (int *)(0x32+offset); адрес содержит переменные, это не строгий абсолютный адрес.

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 появляется на разыменовывании и не проверке Absolute address usage даже при том, что p неподвижные точки к абсолютному адресу.

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

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

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

Поддержка