Exponenta Banner

Неинициализированная локальная переменная

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

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

Описание

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

Примеры

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

#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
Поддержка