pointsto.mlog

module type PROGRAM = sig
  type variable

  type object

  type fieldname

  alloc : variable * object

  assign : variable * variable

  fread : variable * variable * fieldname

  fwrite : variable * fieldname * variable
end

module PointsTo (P : PROGRAM) = struct

  define
    ptsto : P.variable * P.object
    ptsto(?v,?o) :- P.alloc(?v,?o)
    ptsto(?v,?o) :- P.assign(?v,?v2), ptsto(?v2,?o)
    ptsto(?v,?o) :- P.fread(?v,?v2,?f), ptsto(?v2,?o2), fptsto(?o2,?f,?o)

  and
    fptsto : P.object * P.fieldname * P.object
    fptsto(?o,?f,?o2) :- P.fwrite(?v,?f,?v2), ptsto(?v,?o), ptsto(?v2,?o2)

end

module TestProg = struct

  type variable = int

  type object = int

  type fieldname = int

  define
      alloc : int * int
  and assign : int * int
  and fread : int * int * int
  and fwrite : int * int * int

end

module P = PointsTo (TestProg)