Forward conditioned slicing with Frama-C
<p>From the post <a href="https://stackoverflow.com/questions/17572319/understanding-frama-c-slicer-results">Understanding Frama-C slicer results</a>, it seems Frama-C supports the forward conditioned slicing with Frama-C. For the following example test.c, I wonder how to do the forward conditioned slicing with the specific function "event". @Pascal Cuoq</p>

<pre><code>/*@ requires a == 1 ;
*/ 
#include &lt;stdio.h&gt;
int event() { 
   int r;
   scanf("%d", &amp;r); 
   if (r&gt;10) return 1;
   else return 0;
}
void event_process() {
   int x=0; 
   printf("event process\n"); 
   x=1;
} 
void no_event()
{
    int y=0;    
    printf("no event\n");
}
void main ( ) {
   int a; 
   if((a=event()) == 1) 
      event_process();
   else 
      no_event();
   printf("in main\n"); 
   return;
}
</code></pre>

<p>I tried frama-c test.c -slice-calls event -then-on 'Slicing export' -print, why it outputs as follows:</p>

<pre><code>/* Generated by Frama-C */
void event_slice_1(void)
{
  return;
}
void main(void)
{
  event_slice_1();
  return;
}
</code></pre>