一种基于JPF的Java代码SSA单路径的生成方法
摘要:
本发明公开了一种基于JPF的Java代码SSA单路径的生成方法,其特征是包括如下步骤:步骤10:输入.java文件和.jpf文件,存放在src目录下;步骤11:对.java文件进行代码插桩,以便获得path condition;步骤12:编译得到.class文件,存放在bin目录下;步骤13:从.jpf文件获得JPF执行的的相关参数;步骤14:使用JPF的jpf‑symbc模块对.class文件进行符号执行,获取指定方法中的可达的单路径,根据插桩信息提取出path condition;步骤15:使用JDT AST修改单路径代码的AST,将单路径转化为SSA的格式;步骤16:将SSA格式的单路径以及path condition封装成符合Java语法规范的Java类,存放在path目录下,作为输出。
公开/授权文献
0/0