symbolic execution

example1.c

int* func(int x; int y) {
  int* p=0;
  int s=x*y;
  if (s!=0) 
    p=malloc(s);
  else if(y==0) 
    p=malloc(x);
  return p;
}

example2.c

//func as defined above 
int* func(int x; int y);
 
//main calls func 
int main() {  
  int x,y;  
  int p*;  
  ...  
  ASSERT(x!=0);    
  p=func(x,y);  
  ...
}