Polyspace Code Prover

查看范围信息

Polyspace Code Prover 跟踪整个代码的控制逻辑和数据流,并显示与变量和运算符相关联的范围信息。将光标放到运算符或变量上,便会有一条提示消息显示范围信息。形式化方法又称为抽象释义,可以确定精确的范围信息,以便证明软件是否存在某些运行时错误。您可以使用这种范围信息来调试软件,确保某些变量或运算不违反指定的范围限制。

在下面的示例中,Polyspace Code Prover 已确定除法运算左侧操作数的范围是 -1701 至 3276;右侧操作数是 9。除后的结果范围是 -189 至 364。

Tooltip displaying the possible ranges for all run time conditions.
工具提示显示所有运行条件的可能范围。

您可以使用调用层次结构和调用流程图来进一步来显示控制流。

Call flow graph displaying the order of function calls in an interprocedural analysis.

在某过程间分析中的函数调用顺序。

下一页: 跟踪软件质量指标

试用 Polyspace Code Prover

获取试用版软件

Developing Medical Device Software with Zero Bugs

观看网上技术交流会录像