Actions
Bug #9395
closedSymexecute не учитывает неявные преобразования типов в nml моделях
Start date:
11/22/2018
Due date:
% Done:
0%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
Description
В модели RISC-V в массив памяти с 62-х битным индексом производится запись по индексу размерностью 64 бит, что обрабатывается MicroTESK при компиляции и генерации модели, однако Symexecute не учитывает то, что smt-lib таких неявных преобразований не позволяет. Пример из файла riscv_rv32i.nml (строка 350).
tmp_index = tmp_address >> 2;
if tmp_address<1..0> == 0 then // Word-aligned address
tmp_word = MEM[tmp_index];
Генерация smt по данному коду приводит к ошибке солвера:
(error "array select not indexed with correct type for array")
На всякий случай прикладываю бинарный код.
Files
Actions