def specification(self):
    a0 = self.fresh_var(i32, 'a0')
    a1 = self.fresh_var(i32, 'a1')
    a = self.alloc(array_ty(2, i32), points_to=array(a0, a1))
    self.execute_func(a)
    self.points_to(a[0], a1)
    self.points_to(a[1], a0)
    self.returns(void)
def specification(self):
    a0 = self.fresh_var(i32, 'a0')
    a1 = self.fresh_var(i32, 'a1')
    a = self.alloc(array_ty(2, i32), points_to=array(a0, a1))
    self.execute_func(a)
    self.points_to(a[0], a1)
    self.points_to(a[1], a0)
    self.returns(void)