CN: Reduce warnings for experimental tokens

Fixes #574 This shares state implicitly across different lexers, even with `create_lexer`. Threading this state in and out of the lexer is ugly. And we would probably want warnings once per invocation anyway.
rems-project · Dec 12, 2024 · 940e91f · 940e91f
1 parent 7a2f799
commit 940e91f
Show file tree

Hide file tree

Showing 29 changed files with 24 additions and 175 deletions.
diff --git a/parsers/c/c_lexer.mll b/parsers/c/c_lexer.mll
@@ -93,12 +93,12 @@ let lexicon: (string, token) Hashtbl.t =
 
 (* BEGIN CN *)
 
-type kw_kind =
+type cn_keyword_kind =
  | Production
  | Experimental
  | Unimplemented
 
-let cn_keywords: (string * (kw_kind * Tokens.token)) list = [
+let cn_keywords: (string * (cn_keyword_kind * Tokens.token)) list = [
     (* CN 'production' keywords: well-supported and suitable for general use *)
     "good"          , (Production, CN_GOOD);
     "boolean"       , (Production, CN_BOOL);
@@ -164,10 +164,25 @@ let cn_keywords: (string * (kw_kind * Tokens.token)) list = [
     "unpack"        , (Unimplemented, CN_UNPACK);
   ]
 
-let cn_kw_table =
-  let kw_table = Hashtbl.create 0 in
-  List.iter (fun (key, builder) -> Hashtbl.add kw_table key builder) cn_keywords;
-  kw_table
+
+(* This table is mutated during lexing to reduce the number of warnings
+   for experimental features. Unfortunately, this makes it so that the
+   behaviour of the lexer implicitly changes across multiple calls
+   to [create_lexer].
+
+   In some sense, this is fine, since Cerberus/CN only processes one
+   translation unit per invocation from the command line, and we would
+   likely want warnings to only occur once per invocation.
+
+   However, if this were to change, and especially if this were to be
+   made concurrent, this would need to be revisited.
+
+   It is possible to thread the seen experimental tokens back to the caller for
+   them to decide; it is also ugly. *)
+let cn_keywords =
+  let table = Hashtbl.create 0 in
+  List.iter (fun (key, builder) -> Hashtbl.add table key builder) cn_keywords;
+  table
 
 (* Attempt to lex a CN keyword. These may be:
   * 'production' - well-supported and suitable for general use
@@ -177,9 +192,11 @@ let cn_kw_table =
 May raise `Not_found`, indicating `id` is not a recognized CN keyword. *)
 let cn_lex_keyword id start_pos end_pos =
   (* Try to lex CN production keywords *)
-  match Hashtbl.find cn_kw_table id with
+  match Hashtbl.find cn_keywords id with
   | (Production, kw) -> kw
   | (Experimental, kw) ->
+    (* Only want to warn once _per CN/Cerberus invocation_ *)
+    Hashtbl.replace cn_keywords id (Production, kw);
     prerr_endline
       (Pp_errors.make_message
         Cerb_location.(region (start_pos, end_pos) NoCursor)

diff --git a/tests/cn/to_from_bytes_owned.c.verify b/tests/cn/to_from_bytes_owned.c.verify
@@ -5,10 +5,4 @@ tests/cn/to_from_bytes_owned.c:5:9: warning: experimental keyword 'to_bytes' (us
 tests/cn/to_from_bytes_owned.c:9:9: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
     /*@ from_bytes Owned<int>(p); @*/
         ^~~~~~~~~~ 
-tests/cn/to_from_bytes_owned.c:11:9: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-    /*@ to_bytes Owned<int>(p); @*/
-        ^~~~~~~~ 
-tests/cn/to_from_bytes_owned.c:12:9: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-    /*@ from_bytes Owned<int>(p); @*/
-        ^~~~~~~~~~ 
 [1/1]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_copy_memcpy.pass.c.no_annot b/tests/cn_vip_testsuite/pointer_copy_memcpy.pass.c.no_annot
@@ -2,13 +2,7 @@ return code: 0
 tests/cn_vip_testsuite/pointer_copy_memcpy.pass.c:11:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_copy_memcpy.pass.c:12:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Block<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_copy_memcpy.pass.c:14:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_copy_memcpy.pass.c:15:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c.no_annot b/tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c.no_annot
@@ -5,14 +5,8 @@ tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c:28:5: w
 tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c:48:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c:49:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Block<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c:52:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c:53:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
-                ^~~~~~~~~~ 
 [1/2]: user_memcpy -- pass
 [2/2]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c.no_annot b/tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c.no_annot
@@ -2,15 +2,9 @@ return code: 1
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:16:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:17:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:19:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:20:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- fail
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:30:5: error: Missing resource for writing
     *r=11;  // is this free of UB?

diff --git a/tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c.with_annot b/tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c.with_annot
@@ -2,13 +2,7 @@ return code: 0
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:16:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:17:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:19:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c:20:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_from_int_disambiguation_2.pass.c.no_annot b/tests/cn_vip_testsuite/pointer_from_int_disambiguation_2.pass.c.no_annot
@@ -2,13 +2,7 @@ return code: 0
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_2.pass.c:16:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_2.pass.c:17:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_2.pass.c:19:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_2.pass.c:20:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c.no_annot b/tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c.no_annot
@@ -2,15 +2,9 @@ return code: 1
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:16:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:17:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:19:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:20:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- fail
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:34:5: error: Missing resource for writing
     *r=11;  // CN VIP UB if ¬ANNOT

diff --git a/tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c.with_annot b/tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c.with_annot
@@ -2,15 +2,9 @@ return code: 1
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:16:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:17:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:19:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:20:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- fail
 tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:35:7: error: `&copy_alloc_id((u64)&&x[1'u64], copy_alloc_id((u64)value, &y))[(u64)(0'i32 - 1'i32)]` out of bounds
     r=r-1;  // CN VIP UB if NO_ROUND TRIP && ANNOT

diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c.no_annot
@@ -2,15 +2,9 @@ return code: 1
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:21:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:22:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:24:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:25:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- fail
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:33:5: error: Missing resource for writing
     *p = 11; // CN VIP UB (no annot)

diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c.with_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c.with_annot
@@ -2,13 +2,7 @@ return code: 0
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:21:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:22:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:24:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c:25:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c.no_annot
@@ -2,15 +2,9 @@ return code: 1
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:21:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:22:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:24:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:25:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- fail
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:33:5: error: Missing resource for writing
     *p = 11; // CN VIP UB (no annot)

diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c.with_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c.with_annot
@@ -2,13 +2,7 @@ return code: 0
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:21:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:22:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:24:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c:25:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c.no_annot
@@ -2,15 +2,9 @@ return code: 1
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:23:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:24:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:26:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:27:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- fail
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:35:5: error: Missing resource for writing
     *p = 11; // CN VIP UB (no annot)

diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c.with_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c.with_annot
@@ -2,13 +2,7 @@ return code: 0
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:23:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:24:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:26:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c:27:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- pass
diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c.no_annot
@@ -2,15 +2,9 @@ return code: 1
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:23:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:24:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:26:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:27:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- fail
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:35:5: error: Missing resource for writing
     *p = 11; // CN VIP UB (no annot)

diff --git a/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c.with_annot b/tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c.with_annot
@@ -2,13 +2,7 @@ return code: 0
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:23:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:24:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~ 
 tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:26:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
   /*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
                 ^~~~~~~~~~ 
-tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c:27:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
-  /*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
-                ^~~~~~~~~~ 
 [1/1]: main -- pass