From 003d114da9ec4fb511794f7ef9e5e0ed599d1f43 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Sat, 16 Nov 2024 10:15:06 -0600 Subject: [PATCH 1/2] Add local free const to ctx when making subrange constraints --- src/lustre/lustreNodeGen.ml | 1 + tests/regression/success/subrange_local_free_const.lus | 7 +++++++ 2 files changed, 8 insertions(+) create mode 100644 tests/regression/success/subrange_local_free_const.lus diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index 93492e661..af90d610a 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -2367,6 +2367,7 @@ and compile_const_decl ?(ghost = false) cstate ctx map scope = function let ty = Ctx.expand_type_syn ctx ty in if Ctx.type_contains_subrange ctx ty then ( let range_exprs = + let ctx = Ctx.add_ty ctx i ty in AN.mk_range_expr ctx None ty (A.Ident (p, i)) |> List.map fst in List.map (fun expr -> diff --git a/tests/regression/success/subrange_local_free_const.lus b/tests/regression/success/subrange_local_free_const.lus new file mode 100644 index 000000000..2313597ef --- /dev/null +++ b/tests/regression/success/subrange_local_free_const.lus @@ -0,0 +1,7 @@ +type Nat = subrange [0,*] of int; + +node M() returns (); +const C: Nat; +let + check "P1" 0 <= C; +tel \ No newline at end of file From f7c358520ce9d6be4d6ab013cd5f4458b19bb8e7 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Sat, 16 Nov 2024 10:15:27 -0600 Subject: [PATCH 2/2] Do not add proof obligation for subrange free constants --- src/lustre/lustreAstNormalizer.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 6f0abf2c7..aa57e6a7d 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -1194,19 +1194,19 @@ and normalize_node info map let gids7 = locals |> List.filter (function | A.NodeVarDecl (_, (_, id, _, _)) - | A.NodeConstDecl (_, FreeConst (_, id, _)) | A.NodeConstDecl (_, TypedConst (_, id, _, _)) -> let ty = get_type_of_id info node_id id in Ctx.type_contains_subrange ctx ty || Ctx.type_contains_ref ctx ty + | A.NodeConstDecl (_, FreeConst _) | A.NodeConstDecl (_, UntypedConst _) -> false) |> List.fold_left (fun acc l -> match l with | A.NodeVarDecl (p, (_, id, _, _)) - | A.NodeConstDecl (p, FreeConst (_, id, _)) | A.NodeConstDecl (p, TypedConst (_, id, _, _)) -> let ty = get_type_of_id info node_id id in let ty = AIC.inline_constants_of_lustre_type info.context ty in let gids = union acc (mk_fresh_subrange_constraint Local info p (Some node_id) id ty) in union gids (mk_fresh_refinement_type_constraint Local info p (A.Ident (p, id)) ty) + | A.NodeConstDecl (_, FreeConst _) | A.NodeConstDecl (_, UntypedConst _)-> assert false) (empty ()) in