`process_cbmc_output` doesn't seem to check for `Child` process failure

[tedinski]

As a consequence, CBMC crashing is not noticed properly.

The visible behavior looks like normal CBMC output, followed by the Verification Time: 123s line that Kani follows up with.

[YoshikiTakashima]

Similar to #1563. Perhaps we should audit for subprocess calls?

Is the exit code also 0?

[zhassan-aws]

The child exit status seems to get propagated up to the Kani driver correctly, but the driver doesn't act upon it in a clear way. Here's a reproducer:

$ cat 2d_new.rs 
#[cfg_attr(kani, kani::proof, kani::unwind(3))]
fn main() {
    let mut v1: Vec<Vec<i32>> = Vec::new();
    v1.push(vec![1, 2]);
    v1.push(vec![3]);

    let v2: Vec<i32> = v1.into_iter().flatten().collect();
    assert_eq!(v2, vec![1, 2, 3]);
}

$ ulimit -v 25165824; /usr/bin/time --verbose kani 2d_new.rs

<snip>

Runtime Symex: 4.77991s
size of program expression: 97179 steps
slicing removed 53644 assignments
Generated 9663 VCC(s), 5443 remaining after simplification
Runtime Postprocess Equation: 0.103932s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 1.02005s
Running propositional reduction
Post-processing
Out of memory
Verification Time: 108.492065s
Command exited with non-zero status 1
        Command being timed: "kani 2d_new.rs"
        User time (seconds): 2.66
        System time (seconds): 0.35
        Percent of CPU this job got: 2%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 1:51.31
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 160448
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 0
        Minor (reclaiming a frame) page faults: 105168
        Voluntary context switches: 1245
        Involuntary context switches: 6
        Swaps: 0
        File system inputs: 0
        File system outputs: 34048
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 1

So you can see that the exit status is 1, but Kani did not indicate in any way that CBMC failed.