non-compilable slice produced by frama-c
Hello, I've testing some unstructured programs to study how frama-c slicing plugin works, and I've found that the following code snippet produces a wrong (non-compilable) slice.
Program:
#include <stdio.h> /* printf, scanf, NULL */
#include <stdlib.h>
int main(int argc, char **argv) {
int x = 1;
int i = 0;
for (; i < x; i = i + 2){
switch (i){
case 6:
L:
x++;
}
}
if (x + 1 == i) {goto L;};
return x;
}
Frama-c Command:
frama-c code.c -then -eva -then -slice-return main -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode slice.c
Output slice:
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int x = 1;
int i = 0;
while (i < x) {
L: case 6: x ++;
i += 2;
}
if (x + 1 == i) goto L;
return x;
}
I would love to understand what went wrong in the slicing analysis, and if you got any references to the algorithm/technique in which the slicer plugin is based upon also would be highly appreciated.