Помимо вероятного множества проблем с ненадлежащим моделированием, CrossHair не предоставляет этой гарантии.
CrossHair - это неполная система. Внутренне для каждого постусловия он генерирует три возможных результата: «подтверждено», «отклонено» и «неизвестно». Он производит вывод только для «отклоненного» случая; следовательно, отсутствие выходных данных не указывает на проверку заявления.
Почему CrossHair работает таким образом? Две причины:
- CrossHair генерирует «неизвестные» для всех, кроме самых тривиальных случаев. Различие между «неизвестным» и «подтвержденным» не слишком эффективно для большинства разработчиков. (по крайней мере, в настоящее время рефакторинг вашего кода, чтобы сделать его полностью доступным для CrossHair, будет невозможным или уродливым) Обратите внимание, однако, что CrossHair попытается выполнить множество путей выполнения, прежде чем выдать «неизвестный» результат - результат все еще предоставляет некоторые доказательства того, что условие выполняется.
- Подтвержденное различие между неизвестным будет очень нестабильным со временем. CrossHair разработан с нуля, чтобы развиваться. В среднем, SMT решатели станут лучше. CrossHair станет лучше. Но оба поправятся в среднем ; для отдельных случаев, либо может ухудшиться. Чтобы избежать опасений по поводу подтвержденных или неизвестных регрессий, это различие по умолчанию скрыто.
Лучше всего думать о CrossHair как о тестере фазз с помощью решателя.
При этом, если вы все еще хотите посмотреть, какие свойства являются подтверждаемыми, вы можете запросить этот вывод с помощью специальной опции «сообщить все»: crosshair check --report_all [TARGET].