Merge pull request #416 from n-osborne/record-same-fields-test-case

Add test case for record with partially same fields

test/issues/dune.inc

@@ -166,6 +166,27 @@
    ; Syntax sanity check
    (run ocamlc -c %{dep:pattern_inlined_record.mli}))))
 
+(rule
+ (deps
+  %{bin:gospel}
+  (:checker %{project_root}/test/utils/testchecker.exe))
+ (targets record_with_partially_same_fields.gospel)
+ (action
+  (with-outputs-to record_with_partially_same_fields.mli.output
+   (run %{checker} %{dep:record_with_partially_same_fields.mli}))))
+
+(rule
+ (alias runtest)
+ (action
+  (diff record_with_partially_same_fields.mli record_with_partially_same_fields.mli.output)))
+
+(rule
+ (alias test-cmis)
+ (action
+  (chdir %{project_root}
+   ; Syntax sanity check
+   (run ocamlc -c %{dep:record_with_partially_same_fields.mli}))))
+
 (rule
  (deps
   %{bin:gospel}

test/issues/record_with_partially_same_fields.mli

@@ -0,0 +1,12 @@
+(*@ type t = { a: bool; b: integer } *)
+(*@ type r = { a: bool; c: integer } *)
+
+val f : int -> bool
+(*@ ensures let x = { a = true; b = 42 } in true
+ *)
+(* {gospel_expected|
+   [125] File "record_with_partially_same_fields.mli", line 5, characters 20-40:
+         5 | (*@ ensures let x = { a = true; b = 42 } in true
+                                 ^^^^^^^^^^^^^^^^^^^^
+         Error: The record field b does not exist.
+   |gospel_expected} *)