Retrascope

Ты не мог бы описать семантику полей этих классов (или семантику классов в целом)?

Во-первых, обновись до r38. Я перенес часть логики в класс Assignment, класс Statement теперь базовый для него и пока пустой. Соответственно, я поясню семантику классов Substitution, Assignment, BasicBlock, ControlFlowGraph.

Substitution это пара вида "переменная-значение". Фишка в том, что в качестве "переменной" может выступать, например, только один элемент массива, а не весь массив целиком, вот так:

a[0] = '1'

Соответственно, Assignment - это набор таких пар. Например, это может быть одновременное присваивание набору битов некоторого набора значений.

BasicBLock - это набор утверждений. Пока в качестве таковых могут быть только Assignment'ы, потом будут добавлены также вызовы процедур, создание экземпляров модулей и т.п.

ControlFLowGraph - это граф, состоящий из вершин (наследников класса Node - теперь они лежат в отдельном java package) и ребер (Link). Тут уже могут быть не только базовые блоки, но и Switch-и - это условные операторы - и Fork\Join\Merge. Все это надо учитывать при построении Constraint'а.

Игорь, прошу прощения, снова забыл добавить файлы в коммит. r39

Сделал для Substitution и Assignment.
Вопрос по ControlFlowGraph: будет ли класс расширяться? В текущем варианте (когда есть только неупорядоченные наборы узлов и связей), строить Constraint неудобно.

Да, класс будет расширяться и дорабатываться.

Какой constraint следует генерировать в случае WaitStatement?

Никакой. Следует кидать исключение.

Может, лучше перенести implements ISymbolic из Statement в AssignStatement?

Я бы не стал переносить. Вдруг мы все же как-нибудь исхитримся, и начнем строить constraint'ы из wait-выражений?:-)

Пока достаточно просто кидать исключение.