检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
机构地区:[1]上海大学计算机工程与科学学院,上海200072 [2]上海市计算机软件评测重点实验室,上海201112
出 处:《计算机科学》2014年第5期208-214,共7页Computer Science
基 金:国家自然科学基金项目(61073050;61170044)资助
摘 要:控制流图描述了函数执行时可能采取的执行路径。绝大多数静态分析工具都在抽象语法树之上生成控制流图并据此对程序的运行行为进行分析。在模型检测过程中,提取正确的控制流图是构建系统模型的关键。在分析C程序的抽象语法树和控制结构的基础上,设计并实现了程序控制流图提取的算法,并分析了算法的正确性。基于提取的控制流程,可对C程序的某些性质进行模型检验。CFG (Control Flow Graph) represents the execution paths that may be taken in program,and the majority of static analysis tools provide its outcome by extracting control flow graph from AST (Abstract Syntax Tree) and then analyzing the CFG.Extracting correct CFG is the key to build system model on the process of model checking.This paper presented the algorithms for extracting the CFG of functions based on semantic analysis and structure analysis of AST.According to the CFG,some properties of C program can be analyzed via model checking tool.
分 类 号:TP311.5[自动化与计算机技术—计算机软件与理论]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:3.147.46.129