Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CN: Reduce lexer warning #762

Merged
merged 2 commits into from
Dec 12, 2024
Merged

CN: Reduce lexer warning #762

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
087163d
Remove trailing whitespaces from lexer
dc-mak Dec 12, 2024
d2126f4
CN: Reduce warnings for experimental tokens
dc-mak Dec 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions backend/cn/lib/executable_spec_extract.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
71 changes: 44 additions & 27 deletions parsers/c/c_lexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,14 +93,14 @@ let lexicon: (string, token) Hashtbl.t =

(* BEGIN CN *)

type kw_kind =
| Production
| Experimental
| Unimplemented
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);
"good" , (Production, CN_GOOD);
"boolean" , (Production, CN_BOOL);
"integer" , (Production, CN_INTEGER);
"u8" , (Production, CN_BITS (`U,8));
Expand Down Expand Up @@ -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);
Expand All @@ -164,28 +164,45 @@ 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

(* Attempt to lex a CN keyword. These may be:
(* 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
* '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_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)
Errors.(CPARSER (Errors.Cparser_experimental_keyword id))
Warning);
kw
kw
| (Unimplemented, _) -> raise (Error (Errors.Cparser_unimplemented_keyword id))

(* END CN *)
Expand Down Expand Up @@ -588,10 +605,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
}
Expand All @@ -601,10 +618,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
}
Expand All @@ -627,7 +644,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 '@'
Expand Down
6 changes: 0 additions & 6 deletions tests/cn/to_from_bytes_owned.c.verify
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_copy_memcpy.pass.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.pass.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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?
Expand Down
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_from_int_disambiguation_1.annot.c.with_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_from_int_disambiguation_2.pass.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c.with_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c.with_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c.with_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c.no_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 0 additions & 6 deletions tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c.with_annot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading