my last question (understanding frama-c slicer results) on precise example, said, goal know if possible conditioned slicing (forward , backward) frama-c. possible?
more precisely, can't obtain precise slice of program :
/*@ requires >= b; @ assigns \nothing; @ ensures \result == a; */ int example4_instr1(int a, int b){ int max = a; if(a < b) max = b; return max; } is possible, using parameters/options, want in case/in general case?
as pascal mentioned in answer previous question, frama-c's backward , forward slicing based on results of analysis called value analysis. analysis non-relational; means keeps information numeric range of variables, not e.g. difference between 2 variables. thus, not able keep track of inequality a >= b. explains why both branches of test if (a < b) appear followed.
without more information either user (but, in example, nothing write value analysis), or analysis, backward slicing must consider if may or may not taken. unfortunately results in program nothing has been sliced away.
Comments
Post a Comment