Theory ProcSDG

section ‹Instantiation of the SDG locale›

theory ProcSDG imports ValidPaths "../StaticInter/SDG" begin

interpretation Proc_SDG:
  SDG sourcenode targetnode kind "valid_edge wfp" "(Main,Entry)"
  get_proc "get_return_edges wfp" "lift_procs wfp" Main "(Main,Exit)"
  "Def wfp" "Use wfp" "ParamDefs wfp" "ParamUses wfp"
  for wfp ..

end