PointsTo.dl

// propagates inferred properties

.decl PointsTo(src:Variable, dst:Variable)
.output PointsTo

USED("PointsTo-01")
NodeOrigin(src, value) :-
//  REACHABLE(src)
  PointsTo(src, dst),
  NodeOrigin(dst, value).
  // CHECKED

USED("PointsTo-02")
ExternalOrigin(src, value, tn) :-
//  REACHABLE(src)
  ExternalOrigin(dst, value, tn),
  PointsTo(src, dst).
  // CHECKED

USED("PointsTo-03")
PNode(src, pap_f, pap_ar, pap_rem) :-
//  REACHABLE(src)
  PNode(dst, pap_f, pap_ar, pap_rem),
  PointsTo(src, dst).
  // CHECKED

USED("PointsTo-04")
PNodeArgument(src, pap_f, pap_i, pap_value) :-
//  REACHABLE(src)
  PNodeArgument(dst, pap_f, pap_i, pap_value),
  PointsTo(src, dst).
  // CHECKED

// handling of external sub structure result & external sub structure pattern match

.decl TypeVarPointsTo(result:Variable, ty_var:Variable, dst:Variable)
.output TypeVarPointsTo

USED("PointsTo-05")
PointsTo(src, dst) :-
//  REACHABLE(src)
  ExternalOrigin(src, r, t),
  TypeVarPointsTo(r, t, dst).
  // CHECKED