Пусть задача проверяющего модуля — проверка двойного закрытия
файлового дескриптора. Резюме функции
close_file( )
будет состоять
из двух ветвей: в первой ветви (flag
≡
false) никакой дополнительной
информации не хранится, во второй (flag
≡
true) имеется событие за-
крытия файла. При анализе приведенной функции вне контекста вызы-
вающей функции проверяющий модуль не может доказать, что внутри
этой функции дескриптор закрывается во второй раз, поскольку на
всех путях выполнения дескриптор закрывается не более одного раза.
Отсюда следует необходимость выполнения отложенной проверки при
применении резюме этой функции, когда контекст вызова позволит
однозначно определить состояние файлового дескриптора при вызове
fclose(f)
внутри
close_file( )
.
Пусть имеется функция, вызывающая
close_file( )
:
1 void double_close(FILE *file) {
2 fclose(file);
3 close_file(true, file);
4 }
На момент вызова функции
close_file( )
(и применения резюме) де-
скриптор
file
закрыт, т.е. его состояние однозначно определено. Это
означает возможность выполнения отложенной проверки, которая по-
кажет, что происходит закрытие уже закрытого дескриптора. В этом
случае происходит срабатывание, путь к которому необходимо постро-
ить изнутри вызываемой функции. Применение этой схемы в рассма-
триваемом примере проиллюстрировано на рис. 1.
Рассмотрим более общий случай произвольной вложенности вызо-
вов. В случае построения пути изнутри вызываемой функции инфор-
мации об узле срабатывания может оказаться недостаточно, так как
по одному узлу невозможно восстановить всю цепочку вложенных
вызовов. Это объясняется тем, что резюме функции верхнего уровня
хранит ссылки только на узлы следующего уровня вложенности. Для
решения такой задачи проверяющий модуль должен самостоятельно
хранить стек вызовов, для которого строится путь выполнения.
Рассмотрим пример. Модифицируем представленный в предыду-
щем примере набор функций, добавив в него промежуточный вызов:
1 void close_file(bool flag, FILE *f) {
2 . . .
3 if (flag)
4
fclose(f);
5 ...
6 }
7
8 void potential_double_close(bool flag, FILE *file) {
90 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5