Regarding Counterexamples in Outputs

[Liangchen]

Dear Developer,

I want to ask how to interpret the counterexamples in the output of the validator. For example, in the case attached, the validation result is false. I want to know how to interpret the counterexample found by the validator, specifically, what are the initial values of each variable when the validation result is incorrect.

Yours,Liangchen

[Philipp Wendler]

Dear Liangchen,

Am 12.06.24 um 15:08 schrieb Liangchen:

Have a look at Counterexample.1.html. This shows the counterexample and
the variable values are visible when clicking on the "-V-" buttons next
to each statement on the left of the screen.

Greetings
Philipp

--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[Liangchen]

Dear Developers

    Thank you very much,but I still have a question:I now hope to process counterexamples in bulk, so I need to read counterexamples using a program. I would like to extract certain information using a program, specifically what values the elements of an array were assigned during assignments. Is there a way to do this? Also, I looked at the output file Counterexample.1.assignment, but I didn't understand its meaning. Can this file provide information about array assignments?

Yours

Liangchen

[Philipp Wendler]

Dear Liangchen,

Am 14.06.24 um 03:42 schrieb Liangchen:

> Dear Developers
> Thank you very much,but I still have a question:I now hope to process
> counterexamples in bulk, so I need to read counterexamples using a program.
> I would like to extract certain information using a program, specifically
> what values the elements of an array were assigned during assignments. Is
> there a way to do this? Also, I looked at the output file
> Counterexample.1.assignment, but I didn't understand its meaning. Can this
> file provide information about array assignments?

Counterexample.1.assignment.txt is a file that provides low-level
information that results directly from our encoding of the program into
SMT formulas. It is primarily useful for debugging, but I would not
recommend to use it for your purpose.

The standard machine readable way of exporting counterexamples of
software verification is a violation witness, and CPAchecker supports
that. So I recommend to use this. There are two formats, both are
defined here:
https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/
And there is more information about witnesses here:
https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/-/blob/main/doc/README-Literature.md