fo_test.i: call to read() with nondet FD

[ccadar]

Benchmark c/ldv-regression/fo_test.i has the following sequence of calls: int file = l_open("unknown",00); where l_open eventually returns __VERIFIER_nondet_int() ... int a = l_read(file,cbuf,99); where l_read calls read(file, ...)

But read is not defined in the file. This looks to me like an invalid benchmark for Test-Comp, no? I assume read should be defined in the file, similarly to how open is defined.

[ccadar]

@lembergerth , @dbeyer has anyone looked at this? I think this benchmark needs to be removed from Test-Comp.

[lembergerth]

Sorry for the delay. read is part of the standard libraries, so a definition should not be required for the program to be valid. (I guess if we try to establish the rule that all methods must be defined within a benchmark task, we will restrict the current and future benchmark set quite a bit)

At program execution, read will get an arbitrary integer as file-descriptor argument and consequently return a negative value since the read fails, but since the return value is not relevant for error- or branch-coverage, can't it be ignored?