Вышел CompCert 2.0

Что это вообще за хрень? Статический анализ C и clang отлично делает, если кому-то надо лучше — пожалуйста, шлите им патчи. Thread sanitizer и memory sanitizer теперь и в clang, и в GCC есть.

А уж «надёжный» компилятор без отладочной информации — это вообще чепуха полная. Ещё и лицензия проприетарная, вкупе с враньём про надёжность.

clang и gcc никто не собирается верифицировать, в отличие от.

clang и gcc никто не собирается верифицировать, в отличие от.

Что в данном случае означает «верифицировать»?

man формальная верификация

man формальная верификация

Т.е компилятор не поддерживает отладочную информацию, но при этом будет верифицирован как корректный компилятор C? Как будет верифицирован сам стандарт C? Стандартная библиотека? Нафига нужен компилятор без расширений?

В общем все сказки про верификацию этого убожества — это очевидное маркетинговое враньё.

Замечательная каша у вас в голове.

Интересная штука - впервые увидел практическое применение Coq и Caml, да ещё и в одном проекте.

Ух, да там и Xavier Leroy приложился...

это очевидное _маркетинговое_ враньё

«_INRIA_ Non-Commercial License Agreement».

Ага у них лишь маркетинг в голове, будут продвигать также как и «coq enterprise edition» и «ocaml corporate version».

мдяяяя. лучше бы они просто проверятор исходного кода сделали. а компиляторы уже есть, в количестве как минимум аж четырёх штук - gcc, clang, pcc, tcc. теперь пять.

Больше компиляторов, хороших и разных, же :)

Хорошего-то в данном случае нет.

ymn, допиши, что компилятор сам по себе верифицирован, а то непонятно. А это - «дополняющий формальные методы проверки на уровне исходного кода» вообще туманно.

И ещё, допускается свободное использование в обучении и исследованиях. А половина кода dual-licensed под GPL2+.

они сделали, в отличии от тебя.

http://frama-c.com/

compsert не смотрел, но думается мне это связанные проекты.

ты, похоже, идиот. Тебе никогда не хотелось биться головой о стол из-за того, что какой-нибудь очередной гнутый gcc вместо корректного бинарного кода выдаёт падающее говно? Здесь на ЛОРе была как минимум одна новость о дыре в лялексовом ведре, порождённой именно кривостью gcc, который любит выкинуть «лишние» инструкции ради оптимизации. И это далеко не единичный случай - на отличных от x86 платформах gcc очень часто выдаёт полную хрень.

Часто применение новых методов вовсе не связано с необходимостью. То есть, ту же задачу можно решить проверенными старыми надёжными разработками. Но чтобы маркетологам было что говорить на презентации, вводят новинку. Сколько ни пытаюсь понять, где же кок применить можно - ничего реально необходимого, невозможного сделать традиционными способами, - ничего придумать не могу. Скептицизм quiet_readonly разделяю чуть менее чем полностью.

Как будет верифицирован сам стандарт C? Стандартная библиотека?

Исходник на си «elabor»-ируется в исходник Clight, который представляет собой «правильное» подмножество си с уже точно определёнными синтаксисом и семантикой, он уже и верифицируется дальше. То есть не весь сишный код заведётся (duff's device, например — нет).

Ещё на тему «как» — у них на сайте, http://compcert.inria.fr/publi.html.

Ну и Clight это не первая формализация си:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.6755

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.9279

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.124.5712

Нафига нужен компилятор без расширений?

«Part of Leroy’s achievement is that he makes it look like it's not so difficult after all: now that he's found the right architecture for building verified compilers, everyone will know how to do it.» (с) Andrew Appel.

То есть чтобы показать как надо делать такого рода вещь — если это понятно, то дальше можно уже писать и «промышленный» верифицируемый компилятор с расширениями, а gcc и clang могут спать спокойно — маркетологи из INRIA не пройдутъ :)

ты, похоже, идиот

Да как обычно: скорее всего провокация, чтобы объяснили (в порыве праведного гнев) что к чем, получить больше информации.

Но перебор, молча слиться не смог - пошел неадекват.

gcc, clang, pcc, tcc

ICC

любит выкинуть «лишние» инструкции ради оптимизации

man volatile man barriers

Какие линуксоиды такой и линукс.

man volatile man barriers

что volatile и barriers, когда целый вызов memset() выкидывается? Ты предлагаешь на каждый указатель ставить volatile?

Я правильно понимаю что за границы массива в коде на таком компиляторе уже не выедешь? Или как?

Часто применение новых методов вовсе не связано с необходимостью

Есть случаи, когда формальное доказательство корректности необходимо, юридически и/или фактически. Их мало, но это и не продукт для массового применения.

ту же задачу можно решить проверенными старыми надёжными разработками

Что ты считаешь надежной разработкой - gcc, clang, ...? Готов взять на себя административную/уголовную ответственность за их выхлоп, который пойдет на критически важную железку?

Но чтобы маркетологам было что говорить на презентации, вводят новинку

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

да не, за границы массива запросто.

просто верифицированный компилятор как я понимаю гарантирует что он накомпиляет именно то что ты написал на си, а не какой то левый код (из-за ошибки в логике компилятора).

Я правильно понимаю что за границы массива в коде на таком компиляторе уже не выедешь?

Это невозможно статически проверить, кроме простейших случаев.

Готов взять на себя административную/уголовную ответственность за их выхлоп, который пойдет на критически важную железку?

Я не поняла, а кто даст гарантию что не будет неправильно инциализирован указатель? Это какой-то маркетинговый пердеж про супернадежные компиляторы. Тут катят другие подходы, для суперважных железок С и С++ вообще запрещено использовать.

И еще один дебил. Откуда вас тут столько?!?

Вот я читаю «для сборки программ с повышенными требованиями надежности», а теперь я хочу спросить как в убогом от рождения С, эти люди мне обеспечат надежность?

Это невозможно статически проверить, кроме простейших случаев.

Это возможно — индекс массива должен быть не типа size_t, а типа Σ (x : size_t) x < размер_массива.

http://ertos.nicta.com.au/research/l4.verified/

суперважных железок С и С++ вообще запрещено использовать.

откуда дровишки? Минобороны США для суперважных железок вообще котирует вообще только три языка: C, C++ (с большими ограничениями) и Ada.

Я си имел в виду, конечно.

А для C++ - возможно?

Это возможно — индекс массива должен быть не типа size_t, а типа Σ (x : size_t) x < размер_массива.

Поздравляю, ты изобрёл зависимые типы. Только в C их нет.

Ты предлагаешь на каждый указатель ставить volatile?

Volatile как раз не следует применять. Есть же барьеры.

Volatile как раз не следует применять. Есть же барьеры.

как помогут барьеры, если компилятор УБИРАЕТ вызов функции?

http://gcc.gnu.org/bugzilla/show_bug.cgi?id=8537

вот тебе пример. И такое поведение встречается до сих пор (на дворе 2013 год, да).

Проснись уже. Для мишн-критикал апликух сто лет как уже используется ява и ничего кроме ява, про С все забыли как страшный сон.

JPL это расскажи, отродье пидараса.

Это что за нотация, и как её читать?

Сам дурак.

The Java coding standard in its entirety has, in collaboration with Semmle, been implemented in Semmle’s static code analyzer, and is currently being tested on JPL internal projects, including the MSL telemetry and command ground software.

Benefits:

Risk reduction on mission-critical software Rapid development of custom analyses

Klaus Havelund and Gerard J. Holzmann, leaders of NASA JPL's Laboratory for Reliable Software (LaRS).

Ну что, обрыган, будешь еще тут кукарекать про JPL?

Есть ли случаи дружбы этого компилятора с Objective-C ?

А для C++ - возможно?

Либо type level извращения на шаблонах (http://pwparchive.wordpress.com/2012/03/29/dependent-typing-in-c/). Либо enum-ы:

template<size_t n>
struct Ix;

template<>
struct Ix<2> {
    enum class EnumType : size_t {
        zero, one
    };
};

template<>
struct Ix<3> {
    enum class EnumType : size_t {
        zero, one, two
    };
};

template<size_t n, typename A>
A get(std::array<A, n> xs, typename Ix<n>::EnumType i)
{
    return xs[static_cast<size_t>(i)];
}

    std::array<int, 3> xs = {{ 1, 2, 3 }};
    printf("%d\n", get(xs, Ix<3>::EnumType::zero));

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

Поздравляю, ты изобрёл зависимые типы.

С чего это мне их изобретать? https://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A3-types

Тут — изоморфно fin типам и правильным enum-ам.

Только в C их нет.

Ближайший аналог именно такого типа — enum-ы, но они в си сломанные.

https://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A3-types

как помогут барьеры, если компилятор УБИРАЕТ вызов функции?

А нахрена тупить и писать такой код? Там достаточно прочитать память после записи — и «баг» исчезнет.

В общем GCC с -O0 будет делать то же самое, что и это маркетинговое посмешище.

Спасибо.

А нахрена тупить и писать такой код?

это ты здесь тупишь, болезный. Компилятор, изменяющий семантику кода должен гнить в отстойнике вместе с его авторами.

это ты здесь тупишь, болезный. Компилятор, изменяющий семантику кода должен гнить в отстойнике вместе с его авторами.

GCC -O0 не изменяет. Любой оптимизирующий изменяет, если под семантикой кто-то понимает ещё и состояние регистров и памяти.

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

модератор грохнул мой комментарий. Пусть сам тебе теперь отвечает, хуле.

Gcc - основной компилятор для например Mac OS X, Linux, да и для других операционных систем так же. В Мас OS X конечно и LLVM есть, но он тоже родом из gcc.

Так что нелепо критиковать gcc на основе качества генерируемого кода, оно на уровне и проверено временем и используется сообществом.

Филипп Киркоров - ...

Аргумент к популярности можешь засунуть себе глубоко в задницу. Твоё сообщество использует его дай бог на полутора архитектурах с дефолтными опциями. Стоит отойти от этого, и сразу лезут килотонны багов.

В OS X используется старая ветка gcc с кучей собственных патчей, потому что разработчики из GNU не спешат исправлять многие ошибки по причине собственной импотенции.

LLVM - совершенно сторонний, не имеющий никакого отношения к GCC проект (подумай головой, дубина, GCC лицензирован под GPL, а LLVM - нет).