Theory JVMSDG

Up to index of Isabelle/HOL/Jinja/HRB-Slicing

theory JVMSDG
imports JVMCFG_wf JVMPostdomination SDG
theory JVMSDG imports JVMCFG_wf JVMPostdomination "../StaticInter/SDG" begin

interpretation JVMCFGExit_wf_new_type:
CFGExit_wf "sourcenode" "targetnode" "kind" "valid_edgeCFG P"
"(ClassMain (fstCFG P), MethodMain (fstCFG P), None, Enter)"
"(λ(C, M, pc, type). (C, M))" "get_return_edges (fstCFG P)"
"((ClassMain (fstCFG P), MethodMain (fstCFG P)),[],[]) # procs (PROG (fstCFG P))"
"(ClassMain (fstCFG P), MethodMain (fstCFG P))"
"(ClassMain (fstCFG P), MethodMain (fstCFG P), None, Return)"
"Def (fstCFG P)" "Use (fstCFG P)" "ParamDefs (fstCFG P)" "ParamUses (fstCFG P)"
for P
unfolding valid_edge_CFG_def
..

interpretation JVM_SDG :
SDG "sourcenode" "targetnode" "kind" "valid_edgeCFG P"
"(ClassMain (fstCFG P), MethodMain (fstCFG P), None, Enter)"
"(λ(C, M, pc, type). (C, M))" "get_return_edges (fstCFG P)"
"((ClassMain (fstCFG P), MethodMain (fstCFG P)),[],[]) # procs (PROG (fstCFG P))"
"(ClassMain (fstCFG P), MethodMain (fstCFG P))"
"(ClassMain (fstCFG P), MethodMain (fstCFG P), None, Return)"
"Def (fstCFG P)" "Use (fstCFG P)" "ParamDefs (fstCFG P)" "ParamUses (fstCFG P)"
for P
..

end