Почему циклы while, основанные на проверке типов (w/ tc_expr), являются условным выражением?

Question

Кажется, что tc_expr ограничен знанием контекста типизации и ничем иным, поэтому невозможно безопасно "проверить тип" выражения, которое требует знания состояния кучи, например разыменование указателя в качестве условия цикла while. Почему это так и будет ли когда-нибудь возможным для меня доказать правильность цикла, такого как:

char *t = ...;
...
while (*t != 0)
{
    ...
    t++;
}

Я думаю, что в то время как петли можно опционально доказать с изменением tc_expr это допускает разыменование указателя, учитывая контекст кучи вместе с контекстом ввода. Я подозреваю, что мышление состоит в том, что условие цикла должно быть "чистым" выражением, но мне в конечном счете любопытно, действительно ли это необходимое ограничение.

PS Я понимаю, что я мог бы переписать это как для цикла. Мой вопрос все еще стоит, зная, что VST позволяет мне доказать этот вид цикла, хотя и с другим синтаксисом.

Answer 1

Ответ № 1: Это проектное решение, так или иначе, и мы обнаружили, что многие вещи проще (и больше в духе логики разделения), если выражения не обращаются к памяти.

Ответ № 2: Вы можете написать это в то время как цикл, как он есть. Затем используйте Clightgen с -normalize флаг (который вы всегда должны использовать в любом случае), а затем вы можете проверить его. Однако в таком случае форма цикла не будет (строго говоря) циклом Clight "while", она будет иметь свой цикл-тест (if (?) then /*skip*/; else break;в середине тела петли; так что вы будете использовать forward_loop чтобы доказать это, вместо forward_while,