Calls to string functions that are not defined

[ccadar]

Several benchmarks have calls to string functions that are not defined in the benchmark files. For instance, the following benchmarks have calls to strcpy without defining it:

c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i c/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i c/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i

There are benchmarks with similar calls to sprintf, strncmp, strncpy, etc.

Are analysers supposed to provide support for string functions? I assume not, in which case I think the benchmarks either need to define these functions or be removed.

[zvonimir]

For SVCOMP, the rules say that verifiers have to take care of modeling standard library functions. So no definitions will be provided for standard library functions. I suspect that testing competition follows similar rules.

[ccadar]

Thanks, @zvonimir . I don't see this in the Test-Comp rules. Just curious, where is this mentioned in the SV-COMP rules? I grepped for "library" and "standard" in https://sv-comp.sosy-lab.org/2019/rules.php but couldn't find anything.

[zvonimir]

I guess that would be institutional knowledge that is probably not really specified anywhere in the rules. In my experience, there are quite a few things like that that you (hopefully) learn as you go along. Maybe others have better suggestions.

[ccadar]

:) I think it would be really useful to spell these things out, to make it easier for others to get involved. Perhaps such discussions are a good time to update the documentation and rules.

[PhilippWendler]

The SV-COMP rules do mention that the programs are supposed to conform to GNU C or ANSI C, so any functions defined by this standard are allowed.

So I guess this issue can be closed?

[MartinSpiessl]

The same wording is found in the Test-Comp rules:

The programs are assumed to be written in GNU C (some of them adhere to ANSI C). Each program contains all code that is needed for the testing, i.e., no includes (cpp -P). Some programs are provided in CIL (C Intermediate Language) [1].

Potential competition participants are invited to submit benchmark test tasks until the specified date. Test tasks have to fulfill two requirements, to be eligible for the competition: (1) the program has to be written in GNU C or ANSI C, and (2) the program has to come with a specification given by one of the properties stated above. Other specifications are possible, but need to be proposed and discussed.

This issue had two points as far as I can see:

1. Is it documented in SV-COMP/Test-Comp whether these functions need to be implemented?
2. Can the documentation be improved to make it more explicit

The first point should be clear now.

Regarding 2.: @zvonimir @ccadar should this further be improved to explicitly mention the standard library functions? Something like:

Functions from the standard library shall not be implemented in the programs. Instead the verifiers have to ensure that they assign the correct semantics to those functions.

Or are you fine with the status quo?

[ccadar]

@MartinSpiessl I think adding the text you propose is useful and important.

[zvonimir]

I totally agree with @ccadar. I think that such text would be useful to have in the rules.