Add RMC prelude for all tests

[adpaco-aws]

#226 is expected to add an RMC prelude that includes declarations for __nondet() and other verification-related functions. However, it replaces the declaration by the include in a couple of tests only.

Approximate list of functions where this would be needed:

src/test/firecracker/virtio-block-parse/main.rs
src/test/firecracker/micro-http-parsed-request/ignore-main.rs
src/test/firecracker/virtio-balloon-compact/ignore-main.rs
src/test/cargo-rmc/simple-lib/src/lib.rs
src/test/serial/serial2.rs
src/test/serial/serial_spec.rs
src/test/serial/serial.rs
src/test/cbmc/i32-Unary-/main.rs
src/test/cbmc/IfElseifElse_NonReturning/main.rs
src/test/cbmc/FunctionCall_Ret-NoParam/main.rs
src/test/cbmc/FunctionCall_Ret-Param/main.rs
src/test/cbmc/ArithOperators/main.rs
src/test/cbmc/Scopes_NonReturning/main.rs
src/test/cbmc/Bool-BoolOperators/main.rs
src/test/cbmc/LT-GT-LE-GE/main.rs
src/test/cbmc/Scopes_Returning/main.rs
src/test/cbmc/Enum/result3.rs
src/test/cbmc/Cast/from_be_bytes.rs
src/test/cbmc/FloatingPoint/main.rs
src/test/cbmc/IfElseifElse_Returning/main.rs
src/test/cbmc/LoopWhile_NonReturning/main.rs
src/test/cbmc/BitwiseArithOperators/main.rs
src/test/cbmc/BitwiseEqualOperators/main.rs
src/test/cbmc/SaturatingIntrinsics/fixme_128.rs
src/test/cbmc/SaturatingIntrinsics/main.rs
src/test/cbmc/NondetVectors/bytes.rs
src/test/cbmc/NondetVectors/fixme_main.rs
src/test/cbmc/Assume/main.rs
src/test/cbmc/Assume/main_fail.rs
src/test/cbmc/EQ-NE/main.rs
src/test/cbmc/Slice/slice_from_raw_fail.rs
src/test/cbmc/BinOp_Offset/main_fail.rs
src/test/cbmc/LoopLoop_NonReturning/main.rs
src/test/cbmc/ArithEqualOperators/main.rs
src/test/cbmc/Pointers_OtherTypes/main.rs
src/test/smack/loops/iterator_fail.rs
src/test/smack/loops/iterator.rs
src/test/smack/loops/gauss_sum_nondet_fail.rs
src/test/smack/loops/gauss_sum_nondet.rs
src/test/smack/structures/option.rs
src/test/smack/structures/option_fail.rs
src/test/smack/structures/point_fail.rs
src/test/smack/structures/point.rs
src/test/smack/basic/arith_assume2.rs
src/test/smack/basic/arith_assume_fail.rs
src/test/smack/basic/arith_assume.rs
src/test/smack/functions/closure.rs
src/test/smack/functions/closure_fail.rs
src/test/smack/functions/double_fail.rs
src/test/smack/functions/double.rs
src/test/smack/generics/generic_function.rs
src/test/smack/generics/generic_function_fail2.rs
src/test/smack/generics/generic_function_fail4.rs
src/test/smack/generics/generic_function_fail1.rs
src/test/smack/generics/generic_function_fail3.rs
src/test/smack/generics/generic_function_fail5.rs
src/test/prusti/Binary_search_fail.rs
src/test/run-make/gotoc-closure/main.rs
src/test/run-make/gotoc-replace-hashmap/main.rs
src/test/run-make/gotoc-replace-vec/main.rs
src/test/run-make/gotoc-nondet/main.rs
src/test/run-make/gotoc-comp/main.rs
src/test/run-make/gotoc-closure3/main.rs
src/test/run-make/gotoc-dynamic-error-trait/main.rs
src/test/run-make/gotoc-vecdq/main.rs