From 087163d851d50f63b837d0e809d9edfb5d44c9ef Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Thu, 12 Dec 2024 13:33:46 +0000 Subject: [PATCH 1/2] Remove trailing whitespaces from lexer Also silence and ocamlformat warning --- backend/cn/lib/executable_spec_extract.ml | 4 +- parsers/c/c_lexer.mll | 50 +++++++++++------------ 2 files changed, 27 insertions(+), 27 deletions(-) diff --git a/backend/cn/lib/executable_spec_extract.ml b/backend/cn/lib/executable_spec_extract.ml index f038e56bc..2f904b3be 100644 --- a/backend/cn/lib/executable_spec_extract.ml +++ b/backend/cn/lib/executable_spec_extract.ml @@ -56,8 +56,8 @@ let sym_subst (s_replace, bt, s_with) = IT.make_subst [ (s_replace, IT.sym_ (s_with, bt, Cerb_location.unknown)) ] -(** -let concat2 (x : 'a list * 'b list) (y : 'a list * 'b list) : 'a list * 'b list = +(* + let concat2 (x : 'a list * 'b list) (y : 'a list * 'b list) : 'a list * 'b list = let a1, b1 = x in let a2, b2 = y in (a1 @ a2, b1 @ b2) diff --git a/parsers/c/c_lexer.mll b/parsers/c/c_lexer.mll index 173485bb1..9ca05fc86 100644 --- a/parsers/c/c_lexer.mll +++ b/parsers/c/c_lexer.mll @@ -93,14 +93,14 @@ let lexicon: (string, token) Hashtbl.t = (* BEGIN CN *) -type kw_kind = - | Production - | Experimental - | Unimplemented +type kw_kind = + | Production + | Experimental + | Unimplemented let cn_keywords: (string * (kw_kind * Tokens.token)) list = [ (* CN 'production' keywords: well-supported and suitable for general use *) - "good" , (Production, CN_GOOD); + "good" , (Production, CN_GOOD); "boolean" , (Production, CN_BOOL); "integer" , (Production, CN_INTEGER); "u8" , (Production, CN_BITS (`U,8)); @@ -150,7 +150,7 @@ let cn_keywords: (string * (kw_kind * Tokens.token)) list = [ (* CN 'experimental' keywords - functional in some cases but not recommended for general use *) - "cn_list" , (Experimental, CN_LIST); + "cn_list" , (Experimental, CN_LIST); "cn_tuple" , (Experimental, CN_TUPLE); "cn_set" , (Experimental, CN_SET); "cn_have" , (Experimental, CN_HAVE); @@ -164,28 +164,28 @@ let cn_keywords: (string * (kw_kind * Tokens.token)) list = [ "unpack" , (Unimplemented, CN_UNPACK); ] -let cn_kw_table = +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 + List.iter (fun (key, builder) -> Hashtbl.add kw_table key builder) cn_keywords; + kw_table -(* Attempt to lex a CN keyword. These may be: +(* Attempt to lex a CN keyword. These may be: * 'production' - well-supported and suitable for general use - * 'experimental' - functional in some cases but not recommended for general use - * 'unimplemented' - non-functional, but the keyword is reserved + * 'experimental' - functional in some cases but not recommended for general use + * 'unimplemented' - non-functional, but the keyword is reserved May raise `Not_found`, indicating `id` is not a recognized CN keyword. *) -let cn_lex_keyword id start_pos end_pos = +let cn_lex_keyword id start_pos end_pos = (* Try to lex CN production keywords *) - match Hashtbl.find cn_kw_table id with - | (Production, kw) -> kw - | (Experimental, kw) -> - prerr_endline + match Hashtbl.find cn_kw_table id with + | (Production, kw) -> kw + | (Experimental, kw) -> + prerr_endline (Pp_errors.make_message Cerb_location.(region (start_pos, end_pos) NoCursor) Errors.(CPARSER (Errors.Cparser_experimental_keyword id)) Warning); - kw + kw | (Unimplemented, _) -> raise (Error (Errors.Cparser_unimplemented_keyword id)) (* END CN *) @@ -588,10 +588,10 @@ and initial flags = parse | ['A'-'Z']['0'-'9' 'A'-'Z' 'a'-'z' '_']* as id { if flags.inside_cn then - try - cn_lex_keyword id lexbuf.lex_start_p lexbuf.lex_curr_p + try + cn_lex_keyword id lexbuf.lex_start_p lexbuf.lex_curr_p with Not_found -> - UNAME id + UNAME id else UNAME id } @@ -601,10 +601,10 @@ and initial flags = parse Hashtbl.find lexicon id with Not_found -> if flags.inside_cn then - try - cn_lex_keyword id lexbuf.lex_start_p lexbuf.lex_curr_p + try + cn_lex_keyword id lexbuf.lex_start_p lexbuf.lex_curr_p with Not_found -> - LNAME id + LNAME id else LNAME id } @@ -627,7 +627,7 @@ let create_lexer ~(inside_cn:bool) : [ `LEXER of lexbuf -> token ] = match !lexer_state with | LSRegular -> let at_magic_comments = Switches.(has_switch SW_at_magic_comments) in - let magic_comment_char = + let magic_comment_char = if Switches.(has_switch SW_magic_comment_char_dollar) then '$' else '@' From d2126f4486f8c64129fe3134633f0107b3a3f786 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Thu, 12 Dec 2024 14:32:41 +0000 Subject: [PATCH 2/2] 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. --- parsers/c/c_lexer.mll | 31 ++++++++++++++----- tests/cn/to_from_bytes_owned.c.verify | 6 ---- .../pointer_copy_memcpy.pass.c.no_annot | 6 ---- ...r_dataflow_direct_bytewise.pass.c.no_annot | 6 ---- ...from_int_disambiguation_1.annot.c.no_annot | 6 ---- ...om_int_disambiguation_1.annot.c.with_annot | 6 ---- ..._from_int_disambiguation_2.pass.c.no_annot | 6 ---- ...from_int_disambiguation_3.error.c.no_annot | 6 ---- ...om_int_disambiguation_3.error.c.with_annot | 6 ---- ...m_int_subtraction_auto_xy.annot.c.no_annot | 6 ---- ...int_subtraction_auto_xy.annot.c.with_annot | 6 ---- ...m_int_subtraction_auto_yx.annot.c.no_annot | 6 ---- ...int_subtraction_auto_yx.annot.c.with_annot | 6 ---- ...int_subtraction_global_xy.annot.c.no_annot | 6 ---- ...t_subtraction_global_xy.annot.c.with_annot | 6 ---- ...int_subtraction_global_yx.annot.c.no_annot | 6 ---- ...t_subtraction_global_yx.annot.c.with_annot | 6 ---- ...m_ptr_subtraction_auto_xy.error.c.no_annot | 6 ---- ...m_ptr_subtraction_auto_yx.error.c.no_annot | 6 ---- ...ptr_subtraction_global_xy.error.c.no_annot | 6 ---- ...ptr_subtraction_global_yx.error.c.no_annot | 6 ---- .../provenance_basic_auto_yx.error.c.no_annot | 6 ---- ...rovenance_basic_global_yx.error.c.no_annot | 6 ---- ...c_using_uintptr_t_auto_yx.annot.c.no_annot | 6 ---- ...using_uintptr_t_auto_yx.annot.c.with_annot | 6 ---- ...using_uintptr_t_global_yx.annot.c.no_annot | 6 ---- ...ing_uintptr_t_global_yx.annot.c.with_annot | 6 ---- .../provenance_lost_escape_1.annot.c.no_annot | 6 ---- ...rovenance_lost_escape_1.annot.c.with_annot | 6 ---- 29 files changed, 24 insertions(+), 175 deletions(-) diff --git a/parsers/c/c_lexer.mll b/parsers/c/c_lexer.mll index 9ca05fc86..eac9a3e82 100644 --- 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 index 862824933..3e6df251b 100644 --- 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(p); @*/ ^~~~~~~~~~ -tests/cn/to_from_bytes_owned.c:11:9: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*@ to_bytes Owned(p); @*/ - ^~~~~~~~ -tests/cn/to_from_bytes_owned.c:12:9: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*@ from_bytes Owned(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 index 8ca1980fa..5d721c18c 100644 --- 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(&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(&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(&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(&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 index 19236f25e..3318d1b36 100644 --- 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(&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(&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(&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(&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 index 337c08e78..1f3727260 100644 --- 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(&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(&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(&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(&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 index 210e61dec..b9ac428bf 100644 --- 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(&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(&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(&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(&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 index 4bfc43d8c..f95afd65a 100644 --- 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(&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(&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(&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(&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 index e4d756067..307b850cb 100644 --- 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(&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(&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(&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(&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 index d71c5d52d..7e92c5252 100644 --- 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(&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(&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(&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(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c:35:7: error: `©_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 index b61714190..b74bc7642 100644 --- 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(&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(&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(&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(&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 index 0069b3ddb..01b36b274 100644 --- 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(&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(&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(&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(&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 index cc475aa53..6d353cb30 100644 --- 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(&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(&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(&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(&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 index dae5361dd..f9fccfe70 100644 --- 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(&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(&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(&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(&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 index b42a4d87e..1eef026b8 100644 --- 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(&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(&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(&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(&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 index 2422839bd..d9eed5cb3 100644 --- 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(&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(&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(&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(&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 index e4b98e8fb..be53d1282 100644 --- 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(&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(&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(&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(&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 index f3cafd1e4..cb7c78a16 100644 --- 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(&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(&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(&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(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- pass diff --git a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c.no_annot index 70bdfc0ec..d5d92a478 100644 --- a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c.no_annot +++ b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c:12:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&r); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c:13:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c:15:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&r); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c:16:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c:10:22: error: Undefined behaviour ptrdiff_t offset = q - p; // CN VIP UB diff --git a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c.no_annot index 97031e53f..be6bfec79 100644 --- a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c.no_annot +++ b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c:12:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&r); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c:13:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c:15:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&r); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c:16:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c:10:22: error: Undefined behaviour ptrdiff_t offset = q - p; // CN VIP UB diff --git a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c.no_annot index bf6314401..2f890559f 100644 --- a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c.no_annot +++ b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c:14:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&r); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c:15:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c:17:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&r); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c:18:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c:12:22: error: Undefined behaviour ptrdiff_t offset = q - p; // CN VIP UB diff --git a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c.no_annot b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c.no_annot index 247144502..71fe73593 100644 --- a/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c.no_annot +++ b/tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c:14:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&r); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c:15:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c:17:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&r); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c:18:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c:12:22: error: Undefined behaviour ptrdiff_t offset = q - p; // CN VIP UB diff --git a/tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c.no_annot b/tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c.no_annot index e8a3c93c2..a61e8f86b 100644 --- a/tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c.no_annot +++ b/tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c:10:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&p); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c:11:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c:13:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&p); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c:14:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c:19:5: error: Missing resource for writing *p = 11; // CN VIP UB diff --git a/tests/cn_vip_testsuite/provenance_basic_global_yx.error.c.no_annot b/tests/cn_vip_testsuite/provenance_basic_global_yx.error.c.no_annot index 52770dbba..432786655 100644 --- a/tests/cn_vip_testsuite/provenance_basic_global_yx.error.c.no_annot +++ b/tests/cn_vip_testsuite/provenance_basic_global_yx.error.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/provenance_basic_global_yx.error.c:12:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&p); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_global_yx.error.c:13:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_basic_global_yx.error.c:15:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&p); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_global_yx.error.c:16:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/provenance_basic_global_yx.error.c:21:5: error: Missing resource for writing *p = 11; // CN_VIP UB diff --git a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.no_annot b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.no_annot index 178474641..d7febc047 100644 --- a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.no_annot +++ b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:25:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&p); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:26:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:28:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&p); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:29:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:37:5: error: Missing resource for writing *p = 11; // CN VIP UB (no annot) diff --git a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.with_annot b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.with_annot index 88342e382..0b7385b05 100644 --- a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.with_annot +++ b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c.with_annot @@ -2,13 +2,7 @@ return code: 0 tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:25:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&p); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:26:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:28:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&p); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c:29:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- pass diff --git a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.no_annot b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.no_annot index 06e768c20..38bfded08 100644 --- a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.no_annot +++ b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:25:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&p); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:26:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:28:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&p); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:29:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:37:5: error: Missing resource for writing *p = 11; // CN VIP UB (no annot) diff --git a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.with_annot b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.with_annot index 1eb84e572..e58d8f578 100644 --- a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.with_annot +++ b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c.with_annot @@ -2,13 +2,7 @@ return code: 0 tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:25:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&p); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:26:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&q); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:28:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&p); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c:29:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&q); @*/ - ^~~~~~~~~~ [1/1]: main -- pass diff --git a/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.no_annot b/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.no_annot index fe54164b4..8af82288f 100644 --- a/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.no_annot +++ b/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.no_annot @@ -2,15 +2,9 @@ return code: 1 tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:24:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&i1); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:25:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&i4); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:27:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&i1); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:28:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&i4); @*/ - ^~~~~~~~~~ [1/1]: main -- fail tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:30:5: error: Missing resource for writing *q = 11; // CN VIP UB (no annot) diff --git a/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.with_annot b/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.with_annot index d59619ffb..5ef6dc102 100644 --- a/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.with_annot +++ b/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c.with_annot @@ -2,13 +2,7 @@ return code: 0 tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:24:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ to_bytes Owned(&i1); @*/ ^~~~~~~~ -tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:25:17: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ to_bytes Owned(&i4); @*/ - ^~~~~~~~ tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:27:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) /*CN_VIP*//*@ from_bytes Owned(&i1); @*/ ^~~~~~~~~~ -tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c:28:17: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged) - /*CN_VIP*//*@ from_bytes Owned(&i4); @*/ - ^~~~~~~~~~ [1/1]: main -- pass