How to get a slice of data and control dependencies with Frama-c

I tried to do two things

• Get a dynamic backslice based on criteria.
• Match the slice statements to the source code.

Issue 1: shear returned Frama-C, does not return the exact statements that are relevant to the criteria - mainly operators if

and else

.

Problem 2: How to map slicing operators to source code? The program changes when sliced ​​(ex: int a=9

becomes 2 instructions in sliced ​​code int a;

and a = 9;

.) I'm fine with slicing, but what information can I use to map this data against assertions in the source code.

This is the source code.

void main(){
   int ip1 = 9;
   int ip2 = 3;
   int option = 1;
   int result = math(option,ip1,ip2);    
   //@ slice pragma expr ((option == 1) || !(result == (ip1+ip2)));    
 }   

int math(int option, int a, int b){
   int answer = 0;
   if (option == 1){   
     answer = a+b;
   }else{   
     if (option == 2) {   
       answer = a-b;   
     }else { // a ^ b   
       for(int i=0 ;i<b; i++){   
           answer=answer*a;   
       }   
     }
   }
   return answer;
   }

      

        
        
        
      

    

I am using the following command to get a slice.

frama-c t.c -slicing-level 3 -slice-pragma main -slice-print

      

        
        
        
      

    

The layer I get from frama-c is:

void main(void)
{
  int ip1;
  int ip2;
  int option;
  int result;
  ip1 = 9;
  ip2 = 3;
  option = 1;
  result = math_slice_1(ip1,ip2);
  /*@ slice pragma expr option≡1∨!(result≡ip1+ip2); */ ;
  return;
}

int math_slice_1(int a, int b)
{
  int answer;
  answer = a + b;
      return answer;
}

      

        
        
        
      

    

Problem 1: I do not get the conditions if

and else

in the cut. What can I do to get them?

I was expecting the following snippet:

    int math_slice_1(int a, int b)    
    {
      int answer;
       if (option == 1){ 
          answer = a + b; 
       }
      return answer;
    }

      

        
        
        
      

    

Problem 2:
Source Code:int ip1 = 9;

But the sliced ​​code has:

 int ip1;
 ip1 = 9;

      

        
        
        
      

    

How do I map these 2 cut statements to the source code instruction.