Use of `__VERIFIER_nondet_*` functions that aren't specified in SV-COMP rules

[RyanGlScott]

I've noticed that various programs in this repo use __VERIFIER_nondet_* functions that seemingly aren't mentioned anywhere in the SV-COMP rules. I'm using this section of the 2021 SV-COMP rules as a reference:

__VERIFIER_nondet_X(): In order to model nondeterministic values, the following functions can be assumed to return an arbitrary value of the indicated type: __VERIFIER_nondet_X() (and nondet_X(), deprecated) with X in {bool, char, int, float, double, loff_t, long, pchar, pthread_t, sector_t, short, size_t, u32, uchar, uint, ulong, unsigned, ushort} (no side effects, pointer for void *, etc.). The verification tool can assume that the functions are implemented according to the following template: X __VERIFIER_nondet_X() { X val; return val; }

The following programs assume the existence of __VERIFIER_nondet_* that aren't in this list:

• ldv-commit-tester/main0_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa.i uses __VERIFIER_nondet_longlong.
• heap-data/packet_filter.i uses __VERIFIER_nondet_charp.
• ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--rtlwifi--btcoexist--btcoexist.ko-entry_point.cil.out.i uses __VERIFIER_nondet_u8.
• ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--intel--i40evf--i40evf.ko-entry_point.cil.out.i uses __VERIFIER_nondet_u16.

I'm unclear if the rules are incomplete or if these programs aren't following the SV-COMP rules.

[PhilippWendler]

__VERIFIER_nondet_charp can be replaced by __VERIFIER_nondet_pchar. But actually, we removed __VERIFIER_nondet_pointer in the past (https://github.com/sosy-lab/sv-benchmarks/issues/767) and the same reasoning also applies to other pointer-returning nondet methods. So these should probably all be refactored.

For the rest of the methods, the rules should just be extended.