| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_eq_ignore_case/ |
| H A D | aws_byte_cursor_eq_ignore_case_harness.c | 15 __CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_ignore_case_harness()
21 __CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_ignore_case_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_compare_lookup/ |
| H A D | aws_byte_cursor_compare_lookup_harness.c | 20 __CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_compare_lookup_harness()
26 __CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_compare_lookup_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_eq/ |
| H A D | aws_byte_cursor_eq_harness.c | 15 __CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_harness()
21 __CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_compare_lexical/ |
| H A D | aws_byte_cursor_compare_lexical_harness.c | 15 __CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_compare_lexical_harness()
22 __CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE)); in aws_byte_cursor_compare_lexical_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_hash_byte_cursor_ptr/ |
| H A D | aws_hash_byte_cursor_ptr_harness.c | 14 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_CURSOR_SIZE)); in aws_hash_byte_cursor_ptr_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_hash_byte_cursor_ptr_ignore_case/ |
| H A D | aws_hash_byte_cursor_ptr_ignore_case_harness.c | 14 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_hash_byte_cursor_ptr_ignore_case_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_satisfies_pred/ |
| H A D | aws_byte_cursor_satisfies_pred_harness.c | 14 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_satisfies_pred_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_right_trim_pred/ |
| H A D | aws_byte_cursor_right_trim_pred_harness.c | 14 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_right_trim_pred_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_trim_pred/ |
| H A D | aws_byte_cursor_trim_pred_harness.c | 14 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_trim_pred_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_left_trim_pred/ |
| H A D | aws_byte_cursor_left_trim_pred_harness.c | 14 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_left_trim_pred_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_buf_init_copy_from_cursor/ |
| H A D | aws_byte_buf_init_copy_from_cursor_harness.c | 18 __CPROVER_assume(aws_byte_cursor_is_bounded(&cursor, MAX_BUFFER_SIZE)); in aws_byte_buf_init_copy_from_cursor_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_eq_c_str_ignore_case/ |
| H A D | aws_byte_cursor_eq_c_str_ignore_case_harness.c | 16 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_c_str_ignore_case_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_eq_byte_buf_ignore_case/ |
| H A D | aws_byte_cursor_eq_byte_buf_ignore_case_harness.c | 15 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_byte_buf_ignore_case_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_eq_c_str/ |
| H A D | aws_byte_cursor_eq_c_str_harness.c | 16 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_c_str_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_cursor_eq_byte_buf/ |
| H A D | aws_byte_cursor_eq_byte_buf_harness.c | 15 __CPROVER_assume(aws_byte_cursor_is_bounded(&cur, MAX_BUFFER_SIZE)); in aws_byte_cursor_eq_byte_buf_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_buf_append_with_lookup/ |
| H A D | aws_byte_buf_append_with_lookup_harness.c | 19 __CPROVER_assume(aws_byte_cursor_is_bounded(&from, MAX_BUFFER_SIZE)); in aws_byte_buf_append_with_lookup_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_buf_append/ |
| H A D | aws_byte_buf_append_harness.c | 19 __CPROVER_assume(aws_byte_cursor_is_bounded(&from, MAX_BUFFER_SIZE)); in aws_byte_buf_append_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/proofs/aws_byte_buf_write_from_whole_cursor/ |
| H A D | aws_byte_buf_write_from_whole_cursor_harness.c | 18 __CPROVER_assume(aws_byte_cursor_is_bounded(&src, MAX_BUFFER_SIZE)); in aws_byte_buf_write_from_whole_cursor_harness()
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/include/proof_helpers/ |
| H A D | make_common_data_structures.h | 54 bool aws_byte_cursor_is_bounded(const struct aws_byte_cursor *const cursor, const size_t max_size);
|
| /dports/devel/aws-c-common/aws-c-common-0.6.15/verification/cbmc/sources/ |
| H A D | make_common_data_structures.c | 83 bool aws_byte_cursor_is_bounded(const struct aws_byte_cursor *const cursor, const size_t max_size) { in aws_byte_cursor_is_bounded() function
|