qcheck-stm should filter out functions with ghost arguments or results

[shym]

Given the following interface:

type 'a t
(*@ model size : int
    mutable model contents : 'a list *)

val make : int -> 'a -> 'a t
(*@ t = make i a
    checks i >= 0
    ensures t.size = i
    ensures t.contents = List.init i (fun j -> a) *)

val length : 'a t -> int
(*@ i = length [j: int] t
    ensures i = j *)

ortac qcheck-stm array.mli "make 16 'a'" "char t" happily generates the following postcond, in which j is never bound:

    let postcond cmd__004_ state__005_ res__006_ =
      let new_state__007_ = lazy (next_state cmd__004_ state__005_) in
      match (cmd__004_, res__006_) with
      | (Length, Res ((Int, _), i)) -> i = j
      | _ -> true

[shym]

The issue is deeper than just the qcheck-stm plugin. The wrapper will happily generate calls to length j t in the same setting.
We should also consider how to deal with the case in which a function with ghost arguments is marked as pure and is therefore available in other specifications.

[shym]

Closed by #118.