How to get Data & Control Dependency Slice using Frama-c

Question

I was trying to do two things

1. Get a dynamic backward slice based on a criteria.
2. Map the slices statements back to the actual source code.

Problem 1: The slice returned by Frama-C doesn't return the exact statements that were relevant for the criteria - mainly the if and else statements.

Problem 2: How do I map the slicing statements back to the source code? The program gets changed when slicing (for example : int a=9 becomes 2 statements in sliced code int a; and a = 9;.) I am ok with the slice but what is the information I can use to map these back to the statements 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 use the following command to get the slice.

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

The slice 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 dont get the if and else conditions in the slice. What should I do to get them?

I expected the following slice:

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

Problem 2:
Source code has : int ip1 = 9;

But the sliced code has :

 int ip1;
 ip1 = 9;

How to map these 2 sliced statements back to the source code statement.

Answer 1

For Problem 1, the test is sliced out because it is always true since option is set to 1 in the main function. If you want to keep the test, you have to make option an entry (either external global variable or a parameter of main for instance), but then, there will be nothing to slice in the math function... The slicing tries to keep only what is strictly necessary, and the test is not in your case.