Здравствуйте, AlexRK, Вы писали:
ARK>В принципе, идея простая. Можем ли мы сказать, глядя на этот код, что он 100% корректен? Нет. Мы этого не можем утверждать. И верификатор, естественно, тоже не может. Результат? Ошибка компиляции.
<skipped>
Понятно, но выглядит пугающе. Для меня, по крайней мере.
Одним махом уничтожается весь существующий нативный код. Он практически со 100% вероятностью не пройдет эту проверку, а значит, придется переписывать в нем очень многое.
Далее. Представь себе, что это программа линейной алгебры. Там этих a[i][j] в каждой строке может быть по нескольку штук. Если заставлять каждое такое описание верифицировать по твоему механизму — код за этими верификациями видно уже не будет, а отладка превратится в ад.
А не запретишь. И управляемые языки не помогут. Ты же ОС собрался делать, и что, ты мне скажешь, что в этой ОС писать "тяжелый" код можно только на управляемых языках ? Он и без того тяжелый, там O(N^3), например, а мне, выходит, его оптимально написать нельзя ?
Кроме того, почему ты решил, что массив отведен в стеке ? Для него относительно просто написать stack_available. А если в куче ? Да еще двумерный и при этом jagged ? И при этом еще и не прямоугольный, а хорошо если только треугольный ? Тебе не кажется, что такая "статическая" проверка просто не получится ? А еще realloc (в С) есть. А еще union в нем же есть.
Что-то у меня такое ощущение, что это лекарство хуже болезни. Сейчас мне как программисту по крайней мере все ясно — я могу делать (в нативе) что хочу, за свои безобразия в юзермодной части АП я отвечаю сам (кстати, и тут мне помогают, доступ к невыделенным адресам блокируется), а за попытку безобразия в системной части АП будут бить со 100% гарантией. И код я при этом пишу, как его всегда писали. А тут предлагается писать его совсем по-другому, с массой накладных расходов, а успех не гарантирован.
