PP Pavel Putro
- Login: Putro
- Registered on: 07/18/2016
- Last sign in: 10/02/2026
Issues
| open | closed | Total | |
|---|---|---|---|
| Assigned issues | 0 | 3 | 3 |
| Reported issues | 4 | 8 | 12 |
Projects
| Project | Roles | Registered on |
|---|---|---|
| MicroTESK | Developer | 10/06/2017 |
| MicroTESK for PowerPC | Developer | 10/21/2016 |
| MicroTESK for RISC-V | Developer | 11/08/2019 |
| Imperative HOL examples | Manager, Developer, Reporter, Customer | 03/11/2020 |
Activity
09/23/2026
- PP 10:47 AM MicroTESK Bug #13969 (New): Некорректное построение CFG при наличии вызовов функицй
- Используемая модель riscv32 (RV32FULL).
В приложенном примере наблюдается сразу две проблемы построения CFG, которые возможно связаны между собой.
Во-первых алгоритму построения CFG не удаётся определить наличие вызовов функции на ст... - PP 09:28 AM MicroTESK Bug #13968 (Feedback): Декодирование кода из бинарного формата не учитывает assert-ы
- Используемая модель riscv32 (RV32FULL).
Конфликт возникает между инструкциями @c_lui@ и @c_addi16sp@. Эти инструкции делят один опкод и выбор корректной инструкции при декодировании определяется её аргументами. Различить их на уровне мо...
03/23/2021
- PP 04:17 PM MicroTESK Task #10764 (New): Поддержка алтернативного формата вывода SMT-LIB представления машинного кода
- Для использования в рамках задачи SyGuS необходима поддержка формата вывода базовых блоков машинного кода в виде единых функций. Данные функции должны принимать на вход и возвращать единственный параметр типа State, представляющий текуще...
11/10/2020
- PP 12:06 PM MicroTESK Bug #10566 (New): Отсутствует поддержка тернарного оператора в mir
- Наличие тернарного оператора в NML модели приводит к падению при выполнении команды symexecute.
01/13/2020
- PP 05:27 PM MicroTESK for PowerPC Bug #7775 (Closed): Описание MMU инструкций
- PP 05:26 PM MicroTESK for PowerPC Task #7743 (Closed): Коммит 905af510: Sub instruction added
10/02/2019
- PP 12:46 AM MicroTESK Bug #9843 (Closed): MicroTESK версии mir игнорирует параметр binary-file-use-big-endian
- В файле etc/settings.xml присутствует параметр binary-file-use-big-endian, который корректно обрабатывается основной версией инструмента, однако игнорируется версией mir.
Кроме того расположение этого параметра в файле глобальных наст...
08/12/2019
- PP 10:40 PM MicroTESK Bug #9787 (Closed): Некорректное восстановление 64-х битных чисел из памяти.
- Для примера была использована модель risc-v 64-bit. В архиве содержится бинарный и ассемблерный код функции size_test, которая принимает параметром аргумент типа size_t (64-bit) и его же возвращает в качестве результата. Также приложен в...
11/23/2018
- PP 12:58 PM MicroTESK Bug #9395 (Open): Symexecute не учитывает неявные преобразования типов в nml моделях
- Раз неявные преобразования нежелательны, то возможно их стоит запретить на уровне инструмента, чтобы такая ситуация не повторилась в будущем. Ну или всё-таки добавить поддержку в symexecute.
11/22/2018
- PP 02:39 PM MicroTESK Bug #9395 (Closed): Symexecute не учитывает неявные преобразования типов в nml моделях
- В модели RISC-V в массив памяти с 62-х битным индексом производится запись по индексу размерностью 64 бит, что обрабатывается MicroTESK при компиляции и генерации модели, однако Symexecute не учитывает то, что smt-lib таких неявных преоб...