如何过滤由 Frama-C 中的“报告”插件生成的 .csv？答案

【问题标题】：How could I filter .csv generated by "report" plug-in in Frama-C?如何过滤由 Frama-C 中的“报告”插件生成的 .csv？
【发布时间】：2019-06-14 01:30:02
【问题描述】：

目前我正在执行：

frama-c -wp -wp-rte -report-rules test_rules.json -wp-split -wp-fct max -wp-status-maybe -wp-status-invalid -wp-timeout 10 -wp-prover alt-ergo -wp-par 12 -warn-signed-overflow -warn-unsigned-overflow -warn-special-float non-finite test.c -then -report-csv test.csv

我阅读了文档，但没有找到一个很好的解释这个 JSON 文件是如何工作的。我在 GitHub 上找到了一些代码。但对于 Frama-C 新手来说，这仍然不是一件小事。

我想要一个 CSV，它只有状态不同于 Valid 的行，并且只在 test.c 文件中（没有依赖项）。是否可以通过 JSON 配置完成，或者我必须编写自定义解析器？

【问题讨论】：

标签： frama-c

【解决方案1】：

我认为这里存在一些误解：-report-rules 选项旨在与-report-json 一起使用。它对-report-csv 没有影响，它将始终输出整个属性列表。事实上，-report-csv 的重点是将生成的文件导入另一个工具，以便执行您感兴趣的任何操作。例如，您可以简单地在您喜欢的电子表格编辑器及其内置的过滤器。但是也有很多编程选项。基于编写的脚本here，这里是一个使用python 解释器和pandas 库的示例

>>> import pandas
>>> df = pandas.read_csv("test.csv",sep="\t")
>>> print('There are ' + str(len(df)) + ' properties.')
There are 77 properties.
>>> df = df[df['function']=='merge']
>>> print('There are ' + str(len(df)) + ' properties.')
There are 39 properties.
>>> df = df[df['status']=='Unknown']
>> print('There are ' + str(len(df)) + ' properties.')
There are 3 properties.
>>> print('There are ' + str(len(df)) + ' properties.')
>>> df.to_csv(path_or_buf='res.txt',sep='\t')

这为我提供了与文件 res.csv 中的函数 merge 相关的 3 个 Unknown 属性（我没有立即可用的多文件示例，但当然你只需要使用 file第一个查询中的字段）。请记住，“csv”文件实际上是表格分隔的，而不是逗号分隔的（因为逗号往往出现在 ACSL 公式中，后者不太实用）。

【讨论】：