Я, наверное, задолбал этой темой, но, в принципе, можно и

раз в день гонять этот анализ, присылая результаты наутро. В смысле, не так всё отчаянно плохо — можно «договориться» тем или иным образом. Чем-то придётся пожертвовать, но это не так чтобы «совсем бесполезно». Это не win/loose, тут целый спектр.

Если кода достаточно много, даже простая проверка Сшных include guards (тупой regexp, два дня на написание и проверку) выявляет сотни случаев.

Если архитектура анализатора позволяет относительно безболезненно менять абстрактный домен, то уменьшая его мы должны увеличивать производительность. Вроде так?

Это всё ещё про сложные анализы режима "вся программа"?

> можно и раз в день гонять этот анализ, присылая результаты наутро На практике такое работает очень плохо. Основных проблем 2. 1. Наутро разработчики уже забыли, что конкретно они меняли, и вообще, исправления репортов от статического анализатора в бэклоге не было, так что уезжает на какой-нибудь будущий спринт, который никогда не наступит. 2. Если статический анализатор выдаёт достаточно много ложноположительных срабатываний, но между прогонами "забывает" про них (или вообще нет механизма отметить известные ложноположительные случаи) — это очень быстро всем надоест, и на него просто забьют.

Я так понимаю тут сложность будет где-то 4/3 в степени n, где n - число переменных влияющих на результат проверки. Если у вас число превысит 2 в 20 степени, то можно считать, что это не работает.

У нас работает норм. Статический анализ гонится несколько раз в день, если приезжают новые ошибки - сообщение а слак, там тегают автора ошибки и он идёт исправлять. Без беклогов и спринтов, да.

Ваш анализатор использует sat решатель?

Так анализ гоняется на каждый pull request или "от балды"? Блочит мердж или нет? На предмет каких проблем анализирует?

уверенно ничего не понимаю. у нас пивас сейчас, периодически тыкаю палочкой шланг с z3.

От балды, на каждый мр слишком медленно

И примерный объем кода проверяемого ещё напишите для понимания.

------------------------------------------------------------------------------------ Language files blank comment code ------------------------------------------------------------------------------------ C++ 8382 396303 86958 2297196 C/C++ Header 9480 197202 104427 1065150 C# 7278 114689 42557 628749

Не, ну пункт 1 — это болезнь такая. Альцгеймер.

Есть такое понятие — скорость обратной связи.

Я не спорю, что это чудесно. Я вообще люблю, когда обратная связь имеет хотя бы 0.2 сек, а лучше 60 fps. Но я всё клоню к тому, что это не математическая, а инженерная проблема => она не решается на 100%. Но ведь абсолютной неприменимости тоже нет. По Salto ведь даже статьи нет, только презентация. Статью обещали написать. Язык поддерживается не полностью (в смысле, на ряд конструкций стоит failwith "Unimplemented"). В общем, будем посмотреть, что выйдет. Я постараюсь проследить, и, если интересно, рассказать тут.

Whole-program vs. Compositional (modular, incremental) analysis — именно что математическая проблема. Если её "решать инженерными костылями", то результаты будут абы какими. Если статический анализ невозможно встроить в CI, то результаты тоже будут "как получится", потому что проблемы начнут решаться "по возможности, как время будет". Для академических проектов это "приятный бонус", но для индустриальных коммерческих проектов — очень серьёзная проблема.