forked from ocaml-gospel/ortac
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Test warnings triggering and display
Only the warnings of level warning (and not error) are tested in this commit. The generated `.ml` file is ignored because it does not contain relevant information and the OCaml compiler would complain about it.
- Loading branch information
Showing
4 changed files
with
135 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
type 'a t = 'a array | ||
type s = A | ||
|
||
let make = Array.make | ||
let constant = () | ||
let returning_sut a = Array.make 42 a | ||
let no_sut_argument = Fun.id | ||
let multiple_sut_argument _ _ = true | ||
let incompatible_type _ = true | ||
let no_spec _ = true | ||
let impossible_term_substitution _ = true | ||
let ignored_modified _ = () | ||
let ensures_not_found_for_next_state _ = () | ||
let type_not_supported _ = A | ||
let functional_argument _ _ = true | ||
let ghost_argument _ = true | ||
let ghost_returned_value _ = true | ||
let unsupported_quantification _ = true |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
(*@ predicate p (x : 'a) = true *) | ||
|
||
type 'a t | ||
(*@ mutable model contents : 'a list *) | ||
|
||
type s | ||
|
||
val make : int -> 'a -> 'a t | ||
(*@ t = make i a | ||
ensures t.contents = List.init i (fun x -> a) *) | ||
|
||
val constant : unit | ||
(*@ constant | ||
ensures true *) | ||
|
||
val returning_sut : 'a -> 'a t | ||
(*@ t = returning_sut a *) | ||
|
||
val no_sut_argument : bool -> bool | ||
(*@ a = no_sut_argument b *) | ||
|
||
val multiple_sut_argument : 'a t -> 'a t -> bool | ||
(*@ b = multiple_sut_argument x y *) | ||
|
||
val incompatible_type : int t -> bool | ||
(*@ b = incompatible_type t *) | ||
|
||
val no_spec : 'a t -> bool | ||
(*@ b = no_spec t *) | ||
|
||
val impossible_term_substitution : 'a t -> bool | ||
(*@ impossible_term_substitution t | ||
requires old t.contents = [] *) | ||
|
||
val ignored_modified : 'a t -> unit | ||
(*@ ignored_modified t | ||
modifies () *) | ||
|
||
val ensures_not_found_for_next_state : 'a t -> unit | ||
(*@ ensures_not_found_for_next_state t | ||
modifies t.contents *) | ||
|
||
val type_not_supported : 'a t -> s | ||
(*@ s = type_not_supported t *) | ||
|
||
val functional_argument : ('a -> bool) -> 'a t -> bool | ||
(*@ b = functional_argument p t *) | ||
|
||
val ghost_argument : 'a t -> bool | ||
(*@ b = ghost_argument [x : bool] t *) | ||
|
||
val ghost_returned_value : 'a t -> bool | ||
(*@ [ x : bool ], b = ghost_returned_value t *) | ||
|
||
val unsupported_quantification : 'a t -> bool | ||
(*@ b = unsupported_quantification t | ||
ensures b = forall a. List.mem a t.contents -> p a *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
File "testing_warnings.mli", line 12, characters 0-138: | ||
Warning: `constant' is a constant. | ||
|
||
File "testing_warnings.mli", line 16, characters 26-30: | ||
Warning: `returning_sut' returns a sut. | ||
|
||
File "testing_warnings.mli", line 19, characters 22-34: | ||
Warning: `no_sut_argument' have no sut argument. | ||
|
||
File "testing_warnings.mli", line 22, characters 28-48: | ||
Warning: `multiple_sut_argument' have multiple sut arguments. | ||
|
||
File "testing_warnings.mli", line 25, characters 24-29: | ||
Warning: Type of system under test in `incompatible_type' is incompatible with command line argument. | ||
|
||
File "testing_warnings.mli", line 37, characters 13-15: | ||
Warning: Skipping `modifies` `(unit ):unit_1'. | ||
|
||
File "testing_warnings.mli", line 46, characters 27-37: | ||
Warning: Functional argument (`'a -> bool') are not tested. | ||
|
||
File "testing_warnings.mli", line 50, characters 24-25: | ||
Warning: Functions with a ghost argument (`x') are not tested. | ||
|
||
File "testing_warnings.mli", line 53, characters 6-7: | ||
Warning: Functions with a ghost returned value (`x_1') are not tested. | ||
|
||
File "testing_warnings.mli", line 4, characters 18-26: | ||
Warning: No translatable `ensures` clause found to generate `next_state` for model `contents'. | ||
|
||
File "testing_warnings.mli", line 57, characters 16-54: | ||
Warning: unsupported quantification. The clause has not been translated | ||
|
||
File "testing_warnings.mli", line 33, characters 17-18: | ||
Warning: The term `t_1:'a t' can not be substituted (supported only under `old` operator). | ||
|