[Question][Hw5] filter function

[hieudz]

I have a question about the sign domain filter function. For example, we have a code

if( x >= 0) { //<----- x is Top
  ... // some instr, x is untouched here
  if(x < 0) {
    print(x) // <---- should x be neg here?
  }
}

My question is should we assign negative to the x inside the print function? It should be allowed if we define the filter function the same way as in the readme, but it will be wrong for this case because x inside should be Bot?

[RiceBiscuits]

Which an abstract domain did you used in the case?
Top, Pos, Neg, Bot(abstract domain of the homework 5)? or NP, NP, P, N, Z, Top, Bot (abstract domain of the lecture)

I can't catch your question a little bit. Did you mean the answer must be Bot, but the result of filter function of hw5 seems Neg?

[hieudz]

I use the abstract domain of the homework, and yes, you understand my question correctly

[RiceBiscuits]

Can I ask why did you think that the answer is Bot?

[hieudz]

I think there is no number x satisfy both x>= 0 and x<0. So I think x should be bot and the inside code is unreachable (as commented in the example1.c code)

[RiceBiscuits]

If we use an abstract domain of the lecture version, the result can be bot.
And this result seems quite make sense, because print(x) is unreachable.
But in the homework case, the abstract domain is less precise than the lecture version.
Thus, the analyzer cannot treat a sensitive case like your example, so result can be imprecise.

[hieudz]

Thank you a lot. It is clear now