我正在使用frama-c来做一些关于程序切片的实验。该工具很棒,并且有很多不同类型的切片(例如,按结果或按语句)。我正在使用一个程序数据结构,如:
typedef struct ComplexData {
int x;
int y;
char string_[100];
size_t n;
} ComplexData;
这只是一个示例,以便了解frama-c如何根据函数产生的结果对程序进行切片。基本上,main方法调用一个返回ComplexData类型值的函数。如何进行不同执行之间的比较?对结构的每个值进行检查?像这样?