Как я могу отфильтровать .csv, сгенерированный плагином «report» во Frama-C?

Question

В настоящее время я выполняю:

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 или мне нужно написать собственный анализатор?

Answer 1

Я думаю, что здесь есть некоторое недопонимание: опция -report-rules предназначена для использования вместе с -report-json.Это не влияет на -report-csv, что всегда выводит весь список свойств.На самом деле, смысл -report-csv состоит в том, чтобы импортировать полученный файл в другой инструмент, чтобы выполнить любую операцию, которая вас интересует. Например, вы можете просто открыть файл в вашем любимом редакторе электронных таблиц и его встроенномфильтры.Но есть много вариантов программирования.Основываясь на сценарии, написанном здесь , вот пример использования интерпретатора 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')

Это дает мне3 Unknown свойства, относящиеся к функции merge в файле res.csv (у меня не было сразу многофайлового примера, но, конечно, вам просто нужно было бы использовать поле file в первом запросе).Просто имейте в виду, что файл "csv" на самом деле разделен табуляцией и не разделен запятыми (так как запятые, как правило, появляются в формулах ACSL, последний не будет очень практичным).