Да почти то же самое. В Roslyn (компилятор-АПИ для dotNET) ты можешь перекинуть код файла в Sytnax Tree, а код проекта(решения) в Semantic Model.

Собственно, товарищи из PVS-Studio пишут похожие на Infer анализаторы типа "Тут можете словить NullReferenceException", но без каких-то логических систем, просто на Roslyn (читай, на AST).

И поэтому я недоумеваю: вы либо пишите более мощные анализаторы, либо овер-инжинирите решение задачи.

Разумеется, я могу чего-то не понимать.

М-м. Может, на "ты"?

а задача то какая?

если просто "найти некоторые баги" то можно конечно хоть регэкспами искать

Согласен. На том же Roslyn написан пакет "ищущий 100+ некоторых багов". "Возможный NRE", "Условие всегда истинно", "Поле класса нигде не используется", "рискованное замыкание", и т.д.

Энтузиасты пишут анализаторы под баги, специфичные для конкретного проекта. "Если уж вы передаете constructTime параметр в конструктор класса FooBar: указывайте формат даты\времени", "Вы сравниваете два инстанса типа Price, укажите банк, правила которого используются для сравнения".

Какого рода ошибки ищет Infer? Его же не просто так покупают.

ну вообще если вкратце, основная фишка инфера в интерпроцедурном анализе

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

Короче, у PVS сильно больше локальных аналитик, а вы таки пытаетесь искать что-то кросс-методное (интерпроцедурное). Плюс, вы выглядите бесплатными.

А что за математика под капотом? ТеорКат? Автоматы конечные?

во первых не "мы", я к инферу не имею никакого отношения, кроме того что у нас на проекте используется тот же класс логик

отвечая сразу и на второй вопрос - там матлогика, а именно сепарационная логика и так называемый shape analysis через би-абдукцию

поскольку у нас проект заточен под ручной прувинг, шейп анализ, то есть авто-вывод инвариантов мы не используем, но у нас более сложный вариант самой логики

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

или те же хоаровы тройки можно рассматривать в профункторном сеттинге