For this exercise you will build a Z3 model for reaching analysis for the factorial program we have been looking at in class. Reall the factorial program has the following form:
Y := X;
Z := 1;
while 1<Y do
Z := Z * Y;
Y := Y - 1;
Y := 0
In your model you should show that:
X
has not been initiatlized at the end of the programZ
at either label 2 and 4 may reach label 6Z
at label 2 does not reach label 5X
has been assigned before program exit.Each of these may involve one or more assertions and SAT checks based on how you build your model. There are many ways to accomplish this modeling task and I encourage you to be creative!
This project is a warm-up for the next project where you will build a general purpose reaching analysis tool.