Create prototype for smarter CFA-to-C exporter and for simple C language
The goal is to create a new CFA-to-C exporter so that the CFA of a given C program can be exported to a C program as similar as possible to the original program. Ideally, input program and output program will be equal.
For the sake of simplicity, we will first look at loop-free programs with only a single function and without temporary variables.
At the moment, using the CFAToCTranslator
to translate the CFA of a given C program results in an output program that can look very different from the original program.
For example, the following command
scripts/cpa.sh -default -setprop cfa.exportToC=true example.c
with example.c
as follows
int __VERIFIER_nondet_int();
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
int main() {
int i = __VERIFIER_nondet_int();
int c = i;
if (c) {
c = i++;
} else {
while (i < 100) {
i = i + 1;
}
return;
}
if (c >= i) {
ERROR: __VERIFIER_error();
}
}
produces a result file cfa.c
as follows
#include <stdio.h>
#include <assert.h>
extern void __VERIFIER_assume();
extern _Bool __VERIFIER_nondet_bool();
int __VERIFIER_nondet_int();
void __VERIFIER_error();
int main();
int main()
{
int i;
i = __VERIFIER_nondet_int();
int c = i;
if (!(c == 0))
{
int __CPAchecker_TMP_0 = i;
i = i + 1;
c = __CPAchecker_TMP_0;
if (c >= i)
{
ERROR:; __VERIFIER_error();
goto label_2;
}
else
{
label_2:;
goto label_1;
}
}
else
{
label_0:;
if (i < 100)
{
i = i + 1;
goto label_0;
}
else
{
return;
label_1:;
abort();
}
}
}
Edited by Klara Cimbalnik