Exponenta Banner
exponenta event banner

Абсолютное использование адреса

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

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

Описание

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

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

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

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

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

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

Группа: Статическое ЗУ
Язык: C | C++
Акроним: ABS_ADDR
Документация Polyspace Code Prover
Поддержка