[qcheck-stm] Incomplete computation warning

[nikolaushuber]

There seems to be a problem with printing of return values:

$ cat > incomplete_comp.mli << EOF
> type 'a t
> (*@ model contents : 'a list *)
>
> val make : unit -> 'a t 
> (*@ t = make ()
>    ensures t.contents = [] *)
>
> val size : 'a t -> int 
> (*@ s = size t 
>   ensures s = List.length t.contents *)
> EOF
$ cat > incomplete_comp_config.ml << EOF 
> open Incomplete_comp 
> let init_sut = make () 
> type sut = int t
> EOF 
$ ortac qcheck-stm incomplete_comp.mli incomplete_comp_config.ml > /dev/null
File "incomplete_comp.mli", line 8, characters 0-81:
 8 | val size : 'a t -> int 
 9 | (*@ s = size t 
10 |     ensures s = List.length t.contents *)
Warning: Incomplete computation of the returned value in the specification of size. Failure message won't be able to display the expected returned value.

[n-osborne]

Thanks!

I believe the problem comes from here

Gospel sometimes add an fs_apply symbol in the AST that is not handle here.