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:
Xhas not been initiatlized at the end of the program
Zat either label 2 and 4 may reach label 6
Zat label 2 does not reach label 5
Xhas 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.