История изменений
Исправление SZT, (текущая версия) :
Нет, там это как раз можно. Вот например такое, тут просто проветяем, что функция всегда возвращает 1 (т.е. каст из числа из uint64_t в uint8_t равен остатку от деления на 256)
/*@ ensures \result == 1;
*/
uint8_t test_uint8_cast_mod256_eq (uint64_t a)
{
return ((a)%256 == (uint8_t)(a));
}Исправление SZT, :
Нет, там это как раз можно. Вот например такое, тут просто проветяем, что функция всегда возвращает 1 (т.е. каст из числа из uint64_t в uint8_t равен остатку от деления на 256)
/*@ ensures \result == 1;
*/
uint8_t test_uint8_cast_mod256_eq (uint64_t a)
{
return ((a)%256 == (uint8_t)(a));
}Исходная версия SZT, :
Нет, там это как раз можно. Вот например такое, тут просто проветяем, что функция всегда возвращает 1 (т.е. каст из числа из uint64_t в uint8_t равен остатку от деления на 256)
/*@ ensures \result == 1;
*/
uint8_t test_uint8_cast_mod256_eq (uint64_t a)
{
return ((a)%256 == (uint8_t)(a));
}