Skip to content

[BUG] KLEE internal error when generating test with function pointer #478

Open
@tyuldashev

Description

@tyuldashev

To Reproduce
Generate tests for following code:

int compare(const void *a, const void *b) { return (*(char *)a - *(char *)b); }

void my_test(char *str)
{
    qsort(str, strlen(str), sizeof(char), compare);
}

Expected results
Tests are generated without errors

Actual results
Test code starts with following message:

// Some tests for function 'my_test' were skipped, as execution of function leads KLEE to the internal error. See console log for more details.

Server log contains following information:

2022-09-28 14:48:39.062 [t00814305-J1QX  ]      ShellExecTask.cpp:25       1| .   Execute: klee-stats --utbot-config /home/utbot/remote/SampleDocker2/build/utbot_files/klee_out/src/quick_sort_dot_c --table-format=readable-csv 
from directory: /home/utbot/utbot_distr/2022.10.0/utbot_distr
2022-09-28 14:48:39.068 [t00814305-J1QX  ]       BaseForkTask.cpp:73     ERR| .   Exit status: 255
2022-09-28 14:48:39.069 [t00814305-J1QX  ]       BaseForkTask.cpp:74     ERR| .   See details in "/home/utbot/utbot_distr/2022.10.0/utbot_distr/logs/t00814305-J1QX/2022-09-28T11-48-3961.log"
2022-09-28 14:48:39.069 [t00814305-J1QX  ]         KleeRunner.cpp:35     ERR| .   klee-stats call failed:

2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:542      1| .   { parseKTest
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:547      1| .   .   Parse klee for method: compare
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:771      9| .   .   Test case #1:
	return: 0
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:542      1| .   } 0.000 s: parseKTest
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:542      1| .   { parseKTest
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:547      1| .   .   Parse klee for method: my_test
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:771      9| .   .   Test case #1:
	return: 
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:591   WARN| .   .   Don't find object utbot_result in objects array
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:542      1| .   } 0.000 s: parseKTest
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:542      1| .   { parseKTest
2022-09-28 14:48:39.069 [t00814305-J1QX  ]              Tests.cpp:547      1| .   .   Parse klee for method: main
2022-09-28 14:48:39.070 [t00814305-J1QX  ]              Tests.cpp:771      9| .   .   Test case #1:
	return: 0
2022-09-28 14:48:39.070 [t00814305-J1QX  ]              Tests.cpp:542      1| .   } 0.000 s: parseKTest

and t00814305-J1QX/2022-09-28T11-48-3961.log is empty.

Metadata

Metadata

Assignees

Labels

bugSomething isn't workingwrong generationInadequate or empty test suite generated

Type

No type

Projects

Status

Todo

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions