Merge pull request #1105 from daniel-larraz/any-undeclared-type

Fix check of undeclared types in any operators
kind2-mc · Oct 4, 2024 · 9e815c4 · 9e815c4
2 parents 511202d + e800fb4
commit 9e815c4
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/src/lustre/typeCheckerContext.ml b/src/lustre/typeCheckerContext.ml
@@ -807,7 +807,7 @@ and ty_vars_of_type ctx node_name ty =
   | UserType (_, ty_args, id) -> (
     match lookup_ty_syn ctx id ty_args with
     | Some ty -> ty_vars_of_type ctx node_name ty
-    | None -> assert false
+    | None -> SI.empty
   )
   | RefinementType (_, (_, _, ty), e) 
   | ArrayType (_, (ty, e)) -> 

diff --git a/tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus b/tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus
@@ -0,0 +1,4 @@
+node N() returns (y: int);
+let
+  y = any Foo;
+tel
diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml
@@ -599,6 +599,10 @@ let _ = run_test_tt_main ("frontend LustreTypeChecker error tests" >::: [
     match load_file "./lustreTypeChecker/undeclared_type_05.lus" with
     | Error (`LustreTypeCheckerError (_, UndeclaredType _)) -> true
     | _ -> false);
+  mk_test "test undeclared 6" (fun () ->
+    match load_file "./lustreTypeChecker/undeclared_type_06.lus" with
+    | Error (`LustreTypeCheckerError (_, UndeclaredType _)) -> true
+    | _ -> false);
   mk_test "test arity incorrect node call" (fun () ->
     match load_file "./lustreTypeChecker/arity_incorrect_node_call.lus" with
     | Error (`LustreTypeCheckerError (_, IlltypedCall _)) -> true