How to generate counterexample1.c?

[Yoel Kim]

Dear Philipp Wendler,

I was able to find several rules in counterexample1.c:

1. Assignment statements are unchagned;

2. "_[number]" is added to function calls  (e.g., node(); -> node_1();); and

3. Branch statements are converted to assume statements.

I would appreciate it if you could let me know the origin of these rules or if there are any related research papers.

Best regards, 

Yoel Kim

[Philipp Wendler]

Dear Yoel Kim,

Am 18.07.23 um 12:00 schrieb Yoel Kim:

> I was able to find several rules in counterexample1.c:
> 1. Assignment statements are unchagned;
> 2. "_[number]" is added to function calls (e.g., node(); -> node_1();); and
> 3. Branch statements are converted to assume statements.

This will not always be true. For example, CPAchecker will also rewrite
and simplify complex expressions etc.
What precisely is rewritten and how may also change over time.

This output file is mostly intended to be a C representation of the
counterexample for humans and for testing whether the counterexample
exists by execution.
If you want to extract the counterexample path programmatically, we
strongly recommend to use the witness, because this one is written in a
defined format and intended to be machine readable:
https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/

> I would appreciate it if you could let me know the origin of these rules or
> if there are any related research papers.

The origin of how that file is written is purely engineering, there are
no papers about it. There are papers about witnesses, though (linked
from the page above).

Greetings
Philipp

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