Начнём с того, что с Явой я только игрался и поэтому некоторые советы по Яве могут быть не оптимальными.

А что такое отладочный текст?

Текст который не нужен пользователю, но очень помогает создателю программы.

Допустим, расположив в каждой функции вывод в текстовый файл названия функции с параметрами (это чисто пример для понятия) можно узнать как же именно выполнялась наша программа.

который определяет значение и интервал каждой числовой переменной

странная задача. Не имею понятия как чисто из кода определить значение и интервал

Ну например:

читать а

читать в

с = а + в

Можете определить какие значения будут иметь а и в имея только код?

Сам тул верифицирует си-код

Программа не маленькая конечно. Но там должны быть определенные части в которые лезть совсем не нужно.

Программе на вход поступает видимо проект на Си, который читается,разбирается и выуживаются файлы для сканирования.

Затем каждый файл сканируется, при сканировании происходит "преобразование" текста программы в специальные конструкции, а затем эти конструкции уже верифицируются.

Также должна имется часть для чтения/создания правил верификации.

Нужно найти где начало верификаци и в каком виде представлена структура анализируемой программы (должно быть описание по идее)

Фактически, видимо нужно написать еще одно правило верификации. Для этого просто берём уже готовое и переписываем его как требуется.