[CN] `cn --json` can produce non-JSON output

[samcowger]

Consider the following spec (taken from cn-tutorial):

extern struct int_list *mallocIntList();
/*@ spec mallocIntList();
    requires true;
    ensures take u = Block<struct int_list>(return);
            return != NULL;
@*/

With this input, CN will print a warning that "CN pointer equality is not the same as C's", but always pretty-prints this warning, even if --json is specified. There may be other instances of this non-JSON-printing behavior as well.

This behavior presents challenges for tools that expect to consume CN's output in machine-readable form. It would be much easier (and, I would argue, more appropriate) to be able to assume that CN only produces JSON-formatted output.

[samcowger]

This issue also arises when using --batch to check multiple functions - on the example in #287, at least, cn's --batch output is identical whether or not --json is also specified.

This raises an interesting question: how should CN approach printing JSON when it expects to report multiple objects? Should it collect all diagnostics and serialize them as a single object, or as multiple objects in a (probably type-heterogeneous) list? Or should it be able to stream output, printing individual objects in real time with some sort of delimiter between them?

I personally think that supporting streaming output would make CN more easily harnessed by other tools (though I'm far from impartial, since I'm currently working on a language server implementation for CN that harnesses it as a command-line tool), and I think streaming might actually be one of the easier approaches to implement, but I don't know whether it ought to be the default or only behavior - other approaches definitely have merit in other situations.

[septract]

I believe this bug is no longer a blocker, as @samcowger is using CN as a library, rather than calling it through the interface. Probably lower priority as a result