Корныхин Евгений ВМК МГУ Система генерации тестовых программ с использованием ограничений ТЕСЛА
ADD rd, rs, rt LD rt, rt, rs rd=0x0123 rs=0xFA5E … overflow cache hit - overflow - cache miss ожидается: происходит обнаружена ошибка
REGISTER rt, rs, rd, ru: 64; … ADD rt, rs, overflow LD ru, rt, normal(cacheMiss) VAR x: 64; … temp y[31]||y + z[31]||z; ASSERT temp[32] != temp[31]; VAR x: 64; … addr y + z; x Load(addr); тестовый шаблон описания тестовых ситуаций overflow.tslnormal.tsl