cpachecker, CPAchecker,可以配置软件验证平台( 只读镜像)

分享于 

6分钟阅读

GitHub

  繁體 雙語
CPAchecker, the Configurable Software-Verification Platform
  • 源代码名称:cpachecker
  • 源代码网址:http://www.github.com/sosy-lab/cpachecker
  • cpachecker源代码文档
  • cpachecker源代码下载
  • Git URL:
    git://www.github.com/sosy-lab/cpachecker.git
    Git Clone代码到本地:
    git clone http://www.github.com/sosy-lab/cpachecker
    Subversion代码到本地:
    $ svn co --depth empty http://www.github.com/sosy-lab/cpachecker
    Checked out revision 1.
    $ cd repo
    $ svn up trunk
    
    CPAchecker入门

    安装指导: INSTALL.md 插件开发和贡献:doc/Developing.md

    更多文档可以在 doc 插件文件夹中找到。

    通过CPAchecker准备验证程序

    所有程序都需要预先处理 换句话说,前处理器,它们可能不包含 #define 和 #include 指令。 你可以通过在 命令行 上指定-preprocess来启用前处理 inside CPAchecker。 可以给出多个C 文件并将它的链接在一起并作为单个程序( 实验特性) 进行验证。

    CPAchecker能够解析和分析( GNU )的一个大子集。 如果程序的分析失败,请向 cpachecker-users@googlegroups.com 发送报告。

    使用CPAchecker验证程序

    选择要检查的源代码文件。 如果你使用自己的程序,请记住前面提到的上面。 例子:doc/examples/example.c 软件验证是国际软件验证的基准 programs,可以从https://github.com/sosy-lab/sv-benchmarks checked。

    如果要启用谓词分析之类的某些分析,请选择配置文件。 这个文件定义了使用哪个注册会计师。 可以在目录配置/目录中找到标准配置文件。 如果你不希望进行特定的分析,我们推荐 config/default.properties。 但是,注意如果你在 Windows 或者 macOS 上,你需要为这个配置提供专门编译的MathSAT二进制文件。 在 doc/配置中解释了CPAchecker的配置。

    选择规格文件( 你可能不需要在一些注册会计师)。 标准配置文件使用 config/specification/default.spc 作为默认规范。 使用这个,CPAchecker将在源代码文件中查找名为 ERROR ( 不区分大小写) 和断言的标签。 可以在 config/specification/ 中找到其他规范的示例

    执行 scripts/cpa.sh [ -config <CONFIG_FILE> ] [ -spec <SPEC_FILE> ] <SOURCE_FILE> 需要给定配置文件或者规范文件。 当前目录应该是CPAchecker项目目录。 其他 命令行 开关在 doc/configuration中描述。 例如: scripts/cpa.sh -config config/default.properties doc/examples/example.c 这里示例也可以缩写为: scripts/cpa.sh -default doc/examples/example.c 需要使用 Java 1.8兼容的JVM。 如果不在路径中,则需要在环境变量JAVA中指定它。 例如: export JAVA=/usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java 针对Ubuntu的64bit 个 OpenJDK 8. 在 Windows ( witout CYGWIN ) 上,你需要使用 cpa.bat 而不是 cpa.sh ( 在 CYGWIN 环境中工作)。 请注意,并非所有的分析配置都可以用于 Windows ;原因之一是,并非所有解决方案的( 以及用于特定抽象域的其他本地库) 都可以用于 Windows。

    另外,在控制台输出中,在目录 output/ 中生成了交互式的HTML报告,即 Report.html ( 用于结果 true ) 或者 Counterexample.*.html ( 用于结果 false )。 在浏览器中打开这些文件以查看CPAchecker分析结果( cf。 doc/Report.md )

    目录 output/ 中还有其他输出文件:

    • ARG.dot: 抽象可达树( Graphviz格式)的可视化
    • cfa*.dot: 控制控制流自动机( Graphviz格式)的可视化
    • reached.dot: 使用顶部的抽象状态可视化控制流自动机( Graphviz格式)
    • coverage.info: 以 Gcov 格式的覆盖信息( 与测试工具类似) 使用以下 命令行 作为 output/index.html 生成HTML报告: genhtml output/coverage.info --output-directory output --legend
    • Counterexample.*.txt: 通过程序的路径,导致错误
    • Counterexample.*.assignment.txt: 错误路径上所有变量的赋值。
    • predmap.txt: 谓词分析用于验证程序安全性的谓词
    • reached.txt: 所有到达的抽象状态的转储
    • Statistics.txt: 时间统计信息( 也可以用 -stats 打印到控制台)

    注意,并非所有这些文件都可以用于所有配置。 另外,只有在发现错误时才会生成这些文件( ( 反之亦然) )。 CPAchecker将覆盖这里目录中的文件 !


    相关文章