ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
37 stars 10 forks source link

qcheck-stm plugin generates useless with clauses #120

Closed n-osborne closed 1 year ago

n-osborne commented 1 year ago

Given the following interface:

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

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

val set : 'a t -> int -> 'a -> unit
(*@ set t i a
    modifies t.contents
    ensures t.contents = List.mapi (fun j x -> if j = (i : integer) then a else x) (old t.contents) *)

ortac qcheck-stm %{dep:testing.mli} "make 16 'a'" "char t" generates an OCaml file raising warning 23

Error (warning 23 [useless-record-with]): all the fields are explicitly listed in this record:
the 'with' clause is useless.

Either we make the plugin smarter or we ask the user to include 23 in the disabled warnings.