В общем, задача определить, какой путь в программе выбран, а какой - нет, неразрешима. Вполне возможно, что конкретное выражение, как в вашем примере, может иметь указанное значение c. Однако слова «в общем» и «неразрешимый» говорят о том, что вы не можете написать алгоритм, который сможет вычислять значение каждый раз.
На этом этапе алгоритм анализа может быть оптимистичным c или пессимистичным c. Оптимистично c можно выбрать 8 и все будет в порядке - он считает возможным, что во время выполнения x получит это значение. Он также может выбрать 7 - «кто знает, может быть, x будет 7». Но если анализ должен быть надежным, и он не может определить значение условия, он должен предполагать, что первая ветвь может быть взята во время одного выполнения, а вторая ветвь может быть взята во время другого выполнения, поэтому x может быть либо 7, либо 8.
Другими словами, между разумностью и точностью существует компромисс. Или, на самом деле, между разумностью, точностью и решительностью. Последнее свойство сообщает, завершается ли анализ всегда. Теперь вам нужно выбрать то, что нужно:
Решимость - это распространенный выбор для компиляторов и анализаторов кода, потому что вы хотели бы получить ответ о своей программе за конечное время. Однако помощники по доказательству могут запускать некоторые процессы, которые могут работать до указанного предельного времени, и, если ограничение не установлено, навсегда: пользователь может остановить его и попробовать что-то еще.
Надежность - это распространенный выбор для компиляторов, потому что вы хотели бы получить ответ, который соответствует спецификации языка. Анализаторы кода более гибкие. Многие из них несостоятельны, но из-за этого они могут найти больше потенциальных проблем за конечное время, оставляя интерпретацию разработчику. Я полагаю, что упомянутый вами пример говорит об анализе звука.
Точность - это редкое свойство. Компиляторы и анализатор кода должны быть pessimisti c, потому что в противном случае может проникнуть некоторый неправильный код. Но это может быть параметризуемо Например, если компилятор / анализатор поддерживает постоянное распространение и свертывание, и все переменные в примере установлены до некоторых известных констант перед условием, он может вычислить точное значение x после него и быть полностью точным.