[Question][Hw5] Explanation for example1.c

[Ngiong]

Hello.

If I may, can I get an explanation regarding the first example, particularly why z = 10 / x is detected as an error?

int main() {
  int x = source();
  int z;
  if (x >= 0) {
    z = 10 / x; // error
...

Based on my understanding (CMIIW),

• x was initially Top because of int x = source();
• x >= 0 condition causes x = Z or P, but we don't have ZP in our homework so I'm assigning it as Top (?)
• z = 10 / x divisor by Top = not error (or although it's ZP, I think it's not error either (?))

Am I missing something here? Thank you.

-- Minor comment: I thought I followed the lecture quite well, but this homework is still very difficult for me :sob: :sob:

[Altterisk]

Top include Zero, so it's possible to cause division-by-zero error?

[Ngiong]

Oh, I see, I see. I guess you're right because check_instr (located in analysis.ml) classifies an error if the following condition is true: if Memory.Value.order zero v then (In my current understanding, the order function is poset order relational operator ⊑)

By the way, if I changed the condition into neq (i.e., x >= 0 replaced with x != 0) I think now it creates a false positive alarm, because x in the memory is Top, but actually, it's NP. Is my understanding correct?

[Ngiong]

Hello. I think I still need some advice on this particular case :pray: Can I at least get an answer regarding this matter? Or am I really missing some important point here? (If there's something I missed, can I at least get some "guiding pointers" so that I can still learn from this assignment? :sweat_drops: )

cc: @RiceBiscuits

[RiceBiscuits]

Oh, I see, I see. I guess you're right because check_instr (located in analysis.ml) classifies an error if the following condition is true: if Memory.Value.order zero v then (In my current understanding, the order function is poset order relational operator ⊑)

By the way, if I changed the condition into neq (i.e., x >= 0 replaced with x != 0) I think now it creates a false positive alarm, because x in the memory is Top, but actually, it's NP. Is my understanding correct?

Yes. You are right. If the equation is x !=0 (ne) and x is top, then x will be remained top. Because x can be pos or neg in case of this abstract domain. And this roughly abstracted domain can be a cause for false positive.

[Ngiong]

Thank you ^^