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