7 / 22
при моделировании оператора, все эффекты которого учесть по каким-
либо причинам невозможно, например, при вызове функции с недо-
ступным определением.
4. Возврат вызываемой функцией некоторого значения, которое
связывается с выражением вызова функции как элемент окружения.
5. Пометки проверяющих модулей, к которым относятся пометки
символов, регионов памяти и символьных значений, события, которые
необходимо проверить отложенно, когда контекст вызываемой функ-
ции станет достаточно определен для того, чтобы утверждать наличие
потенциального дефекта, и иные действия, связанные с процедурами
проверок (в зависимости от логики работы проверяющего модуля).
Поскольку проверяющие модули самостоятельно отвечают за свои
данные, логику обработки резюме для проверок имеет смысл включать
непосредственно в логику работы этих модулей.
Порождение новых ветвей выполнения программы и отсече-
ние недостижимых путей.
Один из результатов сбора резюме — пары
регион памяти–символьное значение. В результате актуализации сим-
вольных значений из резюме могут получиться символьные значения,
имеющие диапазон, отличный от диапазона этого символьного значе-
ния в контексте вызывающей функции. Это является следствием того,
что при моделировании условий внутри вызываемой функции может
произойти разделение входных данных функции (аргументов и внеш-
них переменных) на классы эквивалентности. Рассмотрим пример.
Пусть вызывается функция
1 void f(int a) {
2 if (a
>
10) {
3 . . .
4 } else {
5 . . .
6 }
7 }
В результате анализа этой функции в ее резюме войдут две ве-
тви выполнения. В первой ветви
a
будет иметь диапазон конкретных
значений от INT_MIN до 10, во второй — от 11 до INT_MAX.
Пусть происходит вызов функции при
a
5. . . 13. Тогда в первой
создаваемой ветви выполнения
а
будет иметь диапазон 5. . . 10, а во
второй — 11. . . 13.
Далее пусть в вызывающей функции
a
имеет диапазон конкрет-
ных значений 5. . . 9. Тогда в первой ветви выполнения
a
будет иметь
диапазон 5. . . 9, а во второй ветви выполнения множество значений
будет пустым. Наличие символического значения с пустым множе-
ством допустимых значений означает, что вторая ветвь недостижима
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5 81