8 / 22
и может не рассматриваться. Действительно, при вызове функции для
заданного
а
выполняется только
else
-ветвь, но не
if
-ветвь.
Введем обозначения:
•
число
n
ветвей выполнения, полученных в резюме анализа вы-
зываемой функции;
•
номер
i
ветви выполнения,
0
6
i < n
;
•
число
p
i
символьных правосторонних входных значений в
i
-й
ветви выполнения;
•
номер
j
символьного значения,
0
6
j < p
i
;
•
символьное значение
s
ij
с номером
j
в
i
-й ветви выполнения;
•
множество значений
r
входные
ij
для значения
s
ij
в контексте вызы-
вающей функции в точке непосредственно перед вызовом функ-
ции;
•
множество значений
r
резюме
ij
для значения
s
ij
в контексте вызы-
ваемой функции;
•
состояние программы
state
входное
в контексте вызывающей функ-
ции в точке непосредственно перед вызовом функции;
•
состояние программы
state
выходное
после вызова функции (после
применения резюме).
Тогда при применении
i
-й ветви выполнения резюме
∀
i
∈
[0;
n
]
,
∀
j
∈
[0;
p
i
] :
r
выходные
ij
=
r
входные
ij
∩
r
резюме
ij
, т.е. результирующее
множество — пересечение множеств входных конкретных значений
символического значения и множества конкретных значений симво-
лического значения из применяемой ветви резюме.
Если результирующее множество конкретных значений является
пустым хотя бы для одного символического значения, то такая ветвь
выполнения недостижима и не принимается в рассмотрение, что мо-
жет быть выражено следующей формулой:
(
∃
i, j
:
r
входные
ij
∩
r
резюме
ij
=
=
∅
)
⇒
(
state
входное
9
state
выходное
)
.
Сбор данных для создания резюме.
Пусть некоторое значение
относится к региону памяти. Поскольку при передаче аргумента функ-
ции не по значению его значение может измениться, необходимо раз-
личать входное значение региона до его изменения в функции и вы-
ходное значение. Для получения информации о разбиении данных
на классы эквивалентности можно отслеживать события ветвлений
(assume), однако это неудобно на практике, так как, во-первых, требует
отдельного отслеживания событий изменений региона для разделения
входных и выходных значений, а, во-вторых — активного участия сбор-
щика резюме в процессе принятия решения о ветвлении. Вместо это-
го в настоящем решении предложен и использован подход, основан-
ный на проверке активности символов и регионов. Входные данные,
внешние по отношении к анализируемой функции, всегда являются
символическими, тогда отслеживая событие потери актуальности (ак-
тивности), можно определить диапазон возможных значений символа,
82 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5