From b5d30a78be56aadb274a87a2944ab46b500b76b3 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 17 Dec 2025 23:47:54 +0000 Subject: [PATCH] EverCDDL: add missing attributes on extract_int, extract_range without these attributes, F* exploded at extraction. With these, the example at https://github.com/project-everest/everparse/issues/248#issue-3711204017 no longer crashes. Thanks @nikswamy for debugging! --- src/cddl/spec/CDDL.Spec.AST.Base.fst | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/cddl/spec/CDDL.Spec.AST.Base.fst b/src/cddl/spec/CDDL.Spec.AST.Base.fst index 9f6e4b4db..a15735f7a 100644 --- a/src/cddl/spec/CDDL.Spec.AST.Base.fst +++ b/src/cddl/spec/CDDL.Spec.AST.Base.fst @@ -512,6 +512,7 @@ let t_size ) ) +[@@sem_attr] let rec extract_int_value (env: sem_env) (x: typ) @@ -532,6 +533,7 @@ let rec extract_int_value | TNamed _ t -> extract_int_value env t | _ -> None +[@@sem_attr] let rec extract_range_value (env: sem_env) (x: typ)