Может ли возвращаемое значение вызова функции быть символическим, чтобы обойти выполнение этой функции?
Я хочу избегать межпроцедурного символического исполнения. Возможно, иметь возвращаемое значение, которое не будет иметь каких-либо ограничений и может разрешить любое возможное конкретное значение.
Возможно ли что-то подобное?
Причина, по которой я хочу сделать это, состоит в том, что я хочу избежать выполнения определенных функций, которые имеют очень очень большой цикл и действительно не изменяют глобальные данные.
2 ответа
Такая функциональность в Klee не реализована. Если вы хотите достичь этого, вы должны выполнить это самостоятельно.
Файл, который вы должны посмотреть, это lib / Core / Executor.cpp. Исполнитель обрабатывает задание для выполнения инструкций символически. Конкретная функция, которую нужно изменить, называется "executeCall". Вы можете проверить название функции. Если это соответствует вашей цели, просто установите программный счетчик на следующую инструкцию и сделайте возвращаемое значение символическим.
С некоторой работой по программированию, я думаю, что ваши потребности достижимы.
Если есть возможность манипулировать исходным кодом, вы можете заменить эти вызовы функций на make_symbolic функция, в которой вы в основном создаете новую символическую переменную и возвращаете ее как возвращение исходного вызова функции. Или вы можете просто переопределить эти функции, чтобы вернуть новое символическое значение.