Compile and run the following C program:

#include <stdio.h>
 
int main() {
  int x;
  int * y;
  y = &x;
  x = 5;
  *y = 9;
  if (x == 5) {
    printf("x is five.\n");
  } else {
    printf("x is not five!\n");
  }
}

What output does the program give?

• here is a random web page talking about pointers in C

Describe in detail how you would modify your symbolic execution engine from Homework 04 to allow you to symbolically execute such C programs and prove which of the two 'if' branches in the program is reachable.

Suppose that C programs can contain the following C statements:

  *x = y
  x = *y
  x = &y

Describe the status of your project. Give a precise mathematical formulation of the question that you tool will answer. Your answer should be at least one half of a page long.