frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-06-05T07:47:25Zhttps://git.frama-c.com/pub/frama-c/-/issues/36non-compilable slice produced by frama-c2023-06-05T07:47:25ZIvan Postolskinon-compilable slice produced by frama-cHello, 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:
```C
#include <stdio.h> /* printf, scanf, ...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:
```C
#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:
```C
/* 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.Patrick BaudinPatrick Baudin