Exponenta Banner

Non-initialized local variable

Локальная переменная не инициализируется прежде чем быть считанным

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

Описание

Эта проверка происходит для каждого чтения локальной переменной. Это определяет, инициализируется ли считанная переменная.

Примеры

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

#include <stdio.h>
    
void main(void) {
   int sum;
   for(int i=1;i <= 10; i++)
      sum+=i;
   printf("The sum of the first 10 natural numbers is %d.", sum);
 }

Оператор sum+=i; сокращение для sum=sum+i;. Поскольку sum используется на правой стороне выражения прежде чем быть инициализированным, проверка Non-initialized local variable возвращает красную ошибку.

Переменная Correction — Initialize перед использованием на правой стороне присвоения

Одна возможная коррекция должна инициализировать sum перед for цикл.

#include <stdio.h>
    
void main(void) {
   int sum=0;
   for(int i=1;i <= 10; i++)
      sum+=i;
   printf("The sum of the first 10 natural numbers is %d.", sum);
 }
#include <stdio.h>
    
int getTerm();
    
void main(void) {
    int count,sum=0,term;
    
    while( count <= 10  && sum <1000) {
       count++;
       term = getTerm();
       if(term > 0 && term <= 1000) sum += term;
      }
    
    printf("The sum of 10 terms is %d.", sum);
 }

В этом примере, переменной count не инициализируется перед сравнением count <= 10. Поэтому проверка Non-initialized local variable возвращает красную ошибку.

Переменная Correction — Initialize перед использованием с оператором отношения

Одна возможная коррекция должна инициализировать count перед сравнением count <= 10.

#include <stdio.h>
    
int getTerm();
    
void main(void) {
    int count=1,sum=0,term;
    
    while( count <= 10  && sum <1000) {
       count++;
       term = getTerm();
       if(term > 0 && term <= 1000) sum+= term;
      }
    
    printf("The sum of 10 terms is %d.", sum);
 }
#include <stdio.h>

int getShift();
int shift(int var) {
    int shiftVal = getShift();
    if(shiftVal > 0 && shiftVal < 1000)
        return(var+shiftVal);
    return 1000;
}
    
void main(void) {
    int initVal;
    printf("The result of a shift is %d",shift(initVal));
}

В этом примере, initVal не инициализируется, когда это передается shift(). Поэтому проверка Non-initialized local variable возвращает красную ошибку. Из-за красной ошибки Polyspace® не проверяет операции в shift().

Переменная Correction — Initialize прежде, чем передать функции

Одна возможная коррекция должна инициализировать initVal прежде, чем передать shift(). initVal может быть инициализирован через функцию ввода. Чтобы избежать переполнения, значение, возвращенное от функции ввода, должно быть внутри границ.

#include <stdio.h>

int getShift();
int getInit();
int shift(int var) {
    int shiftVal = getShift();
    if(shiftVal > 0 && shiftVal < 1000)
        return(var+shiftVal);
    return 1000;
}
    
void main(void) {
   int initVal=getInit();
   if(initVal >0 && initVal < 1000)
     printf("The result of a shift is %d",shift(initVal));
   else
     printf("Value must be between 0 and 1000.");
 }

#include <stdio.h>
#define arrSize 19
 
void main(void)
{
  int arr[arrSize],indexFront, indexBack;
  for(indexFront = 0,indexBack = arrSize - 1; 
    indexFront < arrSize/2; 
    indexFront++, indexBack--) {
    arr[indexFront] = indexFront;
    arr[indexBack] = arrSize - indexBack - 1;
  }
  printf("The array elements are: \n");
  for(indexFront = 0; indexFront < arrSize; indexFront++)
    printf("Element[%d]: %d", indexFront, arr[indexFront]);
 }

В этом примере, в первом for цикл:

  • indexFront запуски от 0 до 8.

  • indexBack запуски от 18 до 10.

Поэтому arr[9] не инициализируется. Во втором for цикл, когда arr[9] передается printf, проверка Non-initialized local variable возвращает ошибку. Ошибка является оранжевой, потому что проверка возвращает ошибку только в одном из запусков цикла.

Из-за оранжевой ошибки в одном из запусков цикла, красная ошибка Non-terminating loop появляется на втором for цикл.

Переменная Correction — Initialize прежде, чем передать функции

Одна возможная коррекция должна сохранить первый for неповрежденный цикл и инициализирует arr[9] вне for цикл.

#include <stdio.h>
#define arrSize 19
 
void main(void)
{
  int arr[arrSize],indexFront, indexBack;
  for(indexFront = 0,indexBack = arrSize - 1;
    indexFront < arrSize/2; 
    indexFront++, indexBack--) {
    arr[indexFront] = indexFront;
    arr[indexBack] = arrSize - indexBack - 1;
  }
  arr[indexFront] = indexFront;
  printf("The array elements are: \n");
  for(indexFront = 0; indexFront < arrSize; indexFront++)
    printf("Element[%d]: %d", indexFront, arr[indexFront]);
}
typedef struct S { 
   int integerField; 
   char characterField;
}S;

void operateOnStructure(S);
void operateOnStructureField(int);

void main() {
  S myStruct;
  operateOnStructure(myStruct);
  operateOnStructureField(myStruct.integerField);
}

В этом примере, структура myStruct не инициализируется. Поэтому, когда структура myStruct передается функциональному operateOnStructure, Non-initialized local variable начинает работу, структура кажется красной.

Коррекция — Инициализирует структуру

Одна возможная коррекция должна инициализировать структуру myStruct прежде, чем передать его функции.

typedef struct S { 
   int integerField; 
   char characterField;
}S;

void operateOnStructure(S);
void operateOnStructureField(int);

void main() {
  S myStruct = {0,' '};
  operateOnStructure(myStruct);
  operateOnStructureField(myStruct.integerField);
}
typedef struct S { 
   int integerField; 
   char characterField;
   double doubleField;
}S;

int getIntegerField(void);
char getCharacterField(void);

void printIntegerField(int);
void printCharacterField(char);

void printFields(S s) {
 printIntegerField(s.integerField);
 printCharacterField(s.characterField);
}

void main() {
  S myStruct;
  
  myStruct.integerField = getIntegerField();
  myStruct.characterField = getCharacterField();
  printFields(myStruct);
}

В этом примере Non-initialized local variable проверяет myStruct является зеленым потому что:

  • Поля integerField и characterField это используется, оба инициализируются.

  • Несмотря на то, что поле doubleField не инициализируется, нет никакой операции чтения или операции записи на поле doubleField в коде.

Чтобы определить, какие поля проверяются на инициализацию:

  1. Выберите проверку на панели Results List или панели Source.

  2. Просмотрите сообщение на панели Result Details.

typedef struct S { 
   int integerField; 
   char characterField;
   double doubleField;
}S;

int getIntegerField(void);
char getCharacterField(void);

void printIntegerField(int);
void printCharacterField(char);
void printDoubleField(double);

void printFields(S s) {
 printIntegerField(s.integerField);
 printCharacterField(s.characterField);
 printDoubleField(s.doubleField);
}

void main() {
  S myStruct;
  
  myStruct.integerField = getIntegerField();
  myStruct.characterField = getCharacterField();
  printFields(myStruct);
}

В этом примере Non-initialized local variable проверяет myStruct является оранжевым потому что:

  • Поля integerField и characterField это используется, оба инициализируются.

  • Поле doubleField не инициализируется и на doubleField существует операция чтения в коде.

Чтобы определить, какие поля проверяются на инициализацию:

  1. Выберите проверку на панели Results List или панели Source.

  2. Просмотрите сообщение на панели Result Details.

int var;

struct s {
    int data;
    int pos;
};

void init_struct(struct s*);
void init_int(int*);

void main (void) {
    struct s s_obj;
    int loc_var;
    
    init_int(&loc_var);
    var =  loc_var;
    
    s_obj.pos = 1;
    init_struct(&s_obj);
    var =  s_obj.data;  
    var = s_obj.pos;    
    
}

В этом примере, определении функций init_int и init_struct не обеспечиваются. Верификация использует тупики в этих функциях. Верификация делает эти предположения для заблокированных функций:

  • Если переменная является неинициализированной или частично инициализированная, функциональные тупики могут уехать, переменные деинициализировали или частично инициализировали. Оранжевый Non-initialized local variable проверяет loc_var и s_obj.data укажите на это потенциально неинициализированное состояние.

  • Если переменная ранее инициализируется, функциональные тупики могут записать различное значение в переменную, но не могут деинициализировать переменную. Зеленый Non-initialized local variable проверяет s_obj.pos укажите на это инициализированное состояние. Если вы устанавливаете свой курсор на pos в var = s_obj.pos, вы видите тот pos может принять любое значение допускало int переменная.

См. также Заблокированные Функции.

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

Группа: Поток данных
Язык: C | C++
Акроним: NIVL

Смотрите также

| |

Темы

Документация Polyspace Code Prover
Поддержка