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

Question

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

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

Это просто пример для того, чтобы понять, как Frama-с может порезать программу по результату производства функции. В принципе, метод main вызывает функцию, которая возвращает значение типа ComplexData. Как выполняется сравнение между различными исполнениями? Есть проверка на каждое значение структуры? Нравится this?

Answer 1

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

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