Исходное сообщение
"Линус Торвальдс не исключил возможность интеграции поддержки..." Отправлено burjui, 25-Июн-22 21:51
Интересные ссылки ты приводишь. А я вот заглянул в другую часть сорцов, и что же я вижу? https://git.codelabs.ch/?p=muen.git;a=blob;f=common/src/sk-c...   27    procedure Cli   28    with   29       Global  => (In_Out => X86_64.State),   30       Depends => (X86_64.State =>+ null),   31       Inline_Always; https://git.codelabs.ch/?p=muen.git;a=blob;f=common/src/sk-c...   37    procedure Cli   38    with   39       SPARK_Mode => Off   40    is   41    begin   42       System.Machine_Code.Asm   43         (Template => "cli",   44          Volatile => True);   45    end Cli; Итого 2 контракта на одну инструкцию "cli" и отключение режима SPARK. То есть, SPARK знать ничего не знает про инструкцию "cli" и никаких гарантий давать не может в принципе, поэтому компилируем функцию как обычную ADA. Ловко выкрутились 😁 Так это что получается, аналог unsafe? Вот тебе и хвалёная верификация. "Мамой клянусь, эта функция только X86_64.State меняет!". Ну что сказать, сильные гарантии. Прямо как в другом языке, где тоже можно из безопасного кода вызывать опасный. Но этот другой язык - плохой, потому что называется Rust, а вот SPARK намного лучше, хотя суть у него та же: разработчик в маленькой функции пообещал не хулиганить, а компилятор пожал плечами и разрешил её вызывать, полагаясь на честное слово.

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:
	Введите код, изображенный на картинке: