[Question][Hw5] Memory at return point

[ShinWonho]

Hello, when implementing return, I have some problems about memory at return point.

In the document, when the instruction is return, it just jump to the return point with current memory.

However, I think it doesn't work well.

In this example, I think x is always 10 at the return point.

In then branch (base case), x is filtered to [10, 10]. Therefore it returns with memory that x is [10,10].

In else branch, it calls f again. And by inductive hypothesis, it returns with memory that x is [10, 10].

So at line number 9, x is always [10, 10], and returns with memory that x is [10, 10].

.

I think, at return point, joining the returned memory and current memory would be sound, but narrowing doesn't work well..

I think I don't understand the semantics well.

Could you explain how to solve this problem??

Thank you.

[h2oche]

I think x is not always [10,10] at line 9, since the value of x doesn't change after function call. By calling f(0), division by zero happens.

[ShinWonho]

Thank you for the comment. I should have considered "context insensitive" analysis!