Нарезка с использованием frama-c

Question

Я использую frama-c, чтобы провести несколько экспериментов по нарезке программ. Инструмент отличный, и есть много разных типов нарезки (например, по результату или по выражению). Я использую структуру данных программы, как:

typedef struct ComplexData {
    int x;
    int y;
    char string_[100];
    size_t n;
} ComplexData;

Это всего лишь пример, чтобы понять, как frama-c может нарезать программу на результат, полученный функцией. По сути, метод main вызывает функцию, которая возвращает значение типа ComplexData. Как проводится сравнение между разными исполнениями? Есть проверка для каждого значения структуры? Как это?

Answer 1

Опция -slice-return f Frama-C инструктирует слайсеру сохранять все операторы, которые способствуют вычислению кода возврата f, Для вашего типа ComplexData, это означает содержание любого из полей. Любое утверждение, которое вычисляет, например, yили один из символов в string_, будут сохранены.

Что касается сравнения между различными исполнениями, статические слайсеры на самом деле работают по-разному. Они аппроксимируют поведение каждой функции во всех возможных исполнениях. (В случае Frama-C это делается с использованием техники, известной как абстрактная интерпретация.) Таким образом, нет необходимости сравнивать два исполнения.