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

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

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

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

Поддержка