diff --git a/x509-parser/.frama-c/GNUmakefile b/x509-parser/.frama-c/GNUmakefile index f928199fa2ba487f7cfd25892f0ae2d31d52e83b..1172e71a36c9ec8e00b143cc1708d89eddbcd12a 100644 --- a/x509-parser/.frama-c/GNUmakefile +++ b/x509-parser/.frama-c/GNUmakefile @@ -20,12 +20,25 @@ FCFLAGS += \ -add-symbolic-path=..:. \ -kernel-warn-key annot:missing-spec=abort \ -kernel-warn-key typing:implicit-function-declaration=abort \ + -warn-left-shift-negative \ + -warn-right-shift-negative \ + -warn-signed-downcast \ + -warn-signed-overflow \ + -warn-unsigned-downcast \ + -warn-unsigned-overflow \ + -wp-dynamic \ ## Eva-specific flags EVAFLAGS += \ -eva-warn-key builtins:missing-spec=abort \ - -eva-precision 1 \ + -eva-precision 2 \ -eva-slevel-function parse_x509_AlgorithmIdentifier:12 \ + -eva-warn-undefined-pointer-comparison none \ + +WPFLAGS += \ + -wp-par 12 \ + -wp-timeout 15 \ + -wp-no-init-const \ ## GUI-only flags FCGUIFLAGS += \ @@ -37,6 +50,25 @@ TARGETS = x509-parser.eva x509-parser.parse: \ ../src/x509-parser.c \ +### This stage runs after Eva, reloading the result from .eva +### Note: some dependencies are hard to include programmatically +### (e.g. the options given to WP), so you may need to +### manually delete the .frama-c/x509-parser.wp directory +### to re-run WP. +x509-parser.wp: x509-parser.eva + mkdir -p $@ + $(FRAMAC) -load $^/framac.sav \ + -kernel-log w:$@/warnings.log \ + -wp-log w:$@/warnings.log \ + -wp $(WPFLAGS) -save $@/framac.sav \ + -then \ + -report-csv $@/alarms.csv \ + +x509-parser.wp.gui: x509-parser.wp + $(FRAMAC)-gui -load $^/framac.sav + +wp: x509-parser.wp + ### Epilogue. Do not modify this block. ####################################### include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk ############################################################################### diff --git a/x509-parser/.frama-c/x509-parser.eva/alarms.csv b/x509-parser/.frama-c/x509-parser.eva/alarms.csv index 0d36c430dc23b103ac59ad963479402e22664c7c..48436a1f490206626c5da0ab7fc719b3d1dbc63b 100644 --- a/x509-parser/.frama-c/x509-parser.eva/alarms.csv +++ b/x509-parser/.frama-c/x509-parser.eva/alarms.csv @@ -14,9 +14,7 @@ src x509-parser.c 132 _extract_complex_tag mem_access Unknown \valid_read(buf + src x509-parser.c 146 _extract_complex_tag user assertion Unknown (*(buf + (len - 1)) & 0x80) ≢ 0 src x509-parser.c 182 get_identifier precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 190 get_identifier postcondition Unknown \result ≡ 0 ⇒ 0 < *\old(eaten) ≤ \old(len) -src x509-parser.c 192 get_identifier postcondition Unknown \result ≡ 0 ⇒ *\old(prim) ≤ 0x1 src x509-parser.c 193 get_identifier postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 206 get_identifier ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 224 get_identifier mem_access Unknown \valid_read(buf + 0) src x509-parser.c 260 get_identifier user assertion Unknown len ≥ rbytes ∧ len - rbytes ≤ 65535 ∧ \valid_read(buf + (rbytes .. len - 1)) src x509-parser.c 263 get_identifier precondition of _extract_complex_tag Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -25,7 +23,6 @@ src x509-parser.c 298 get_length postcondition Unknown \result ≡ 0 ⇒ 0 < *\o src x509-parser.c 299 get_length postcondition Unknown \result ≡ 0 ⇒ *\old(adv_len) ≤ \old(len) src x509-parser.c 300 get_length postcondition Unknown \result ≡ 0 ⇒ *\old(adv_len) + *\old(eaten) ≤ \old(len) src x509-parser.c 301 get_length postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 311 get_length ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 323 get_length user assertion Unknown \valid_read(buf + 0) src x509-parser.c 346 get_length user assertion Unknown *eaten + *adv_len ≤ len src x509-parser.c 394 get_length mem_access Unknown \valid_read(buf + 1) @@ -38,16 +35,19 @@ src x509-parser.c 490 parse_id_len postcondition Unknown \result ≡ 0 ⇒ 1 < * src x509-parser.c 491 parse_id_len postcondition Unknown \result ≡ 0 ⇒ *\old(content_len) ≤ \old(len) src x509-parser.c 492 parse_id_len postcondition Unknown \result ≡ 0 ⇒ *\old(content_len) + *\old(parsed) ≤ \old(len) src x509-parser.c 493 parse_id_len postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 508 parse_id_len ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 522 parse_id_len precondition of get_identifier Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 527 parse_id_len user assertion Unknown cur_parsed > 0 +src x509-parser.c 548 parse_id_len unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)cur_parsed) src x509-parser.c 552 parse_id_len precondition of get_length Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 561 parse_id_len unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)cur_parsed) src x509-parser.c 592 parse_explicit_id_len precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 597 parse_explicit_id_len postcondition Unknown \result ≡ 0 ⇒ *\old(parsed) ≤ \old(len) src x509-parser.c 598 parse_explicit_id_len postcondition Unknown \result ≡ 0 ⇒ *\old(data_len) ≤ \old(len) src x509-parser.c 599 parse_explicit_id_len postcondition Unknown \result ≡ 0 ⇒ *\old(data_len) + *\old(parsed) ≤ \old(len) src x509-parser.c 620 parse_explicit_id_len precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 628 parse_explicit_id_len unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)hdr_len) src x509-parser.c 632 parse_explicit_id_len precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 639 parse_explicit_id_len unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)hdr_len) src x509-parser.c 659 _parse_arc precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 664 _parse_arc postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 666 _parse_arc postcondition Unknown \old(len) > 0 ∧ \old(buf) ≢ \null ∧ \result ≢ 0 ⇒ (∀ ℤ x; 0 ≤ x < \min(\old(len), 4) ⇒ (*(\old(buf) + x) & 0x80) ≢ 0) @@ -57,16 +57,16 @@ src x509-parser.c 725 _parse_arc user assertion Unknown (*(buf + (len - 1)) & 0x src x509-parser.c 748 parse_OID precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 752 parse_OID postcondition Unknown \result ≡ 0 ⇒ 2 < *\old(parsed) ≤ \old(len) src x509-parser.c 753 parse_OID postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 765 parse_OID ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 771 parse_OID precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 778 parse_OID unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)hdr_len) src x509-parser.c 785 parse_OID user assertion Unknown \valid_read(buf + (0 .. data_len - 1)) src x509-parser.c 792 parse_OID loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 809 parse_OID precondition of _parse_arc Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 815 parse_OID user assertion Unknown rbytes ≤ remain +src x509-parser.c 820 parse_OID unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)rbytes) src x509-parser.c 849 parse_integer precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 853 parse_integer postcondition Unknown \result ≡ 0 ⇒ 2 < *\old(eaten) ≤ \old(len) src x509-parser.c 854 parse_integer postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 866 parse_integer ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 872 parse_integer precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 899 parse_integer mem_access Unknown \valid_read(buf + 0) src x509-parser.c 899 parse_integer mem_access Unknown \valid_read(buf + 1) @@ -74,7 +74,6 @@ src x509-parser.c 905 parse_integer mem_access Unknown \valid_read(buf + 1) src x509-parser.c 931 parse_boolean precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 935 parse_boolean postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 936 parse_boolean postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 944 parse_boolean ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 956 parse_boolean mem_access Unknown \valid_read(buf + 0) src x509-parser.c 956 parse_boolean mem_access Unknown \valid_read(buf + 1) src x509-parser.c 962 parse_boolean mem_access Unknown \valid_read(buf + 2) @@ -85,64 +84,58 @@ src x509-parser.c 1014 parse_x509_Version precondition of parse_explicit_id_len src x509-parser.c 1060 parse_CertificateSerialNumber precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1064 parse_CertificateSerialNumber postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 1065 parse_CertificateSerialNumber postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 1076 parse_CertificateSerialNumber ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 1083 parse_CertificateSerialNumber precondition of parse_integer Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1100 parse_CertificateSerialNumber mem_access Unknown \valid_read(buf + 2) src x509-parser.c 1119 parse_CertificateSerialNumber mem_access Unknown \valid_read(buf + 2) src x509-parser.c 1685 parse_algoid_params_ecdsa_with precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1689 parse_algoid_params_ecdsa_with postcondition Unknown \old(buf) ≢ \null ∧ \old(len) ≡ 0 ⇒ \result ≡ 0 src x509-parser.c 1690 parse_algoid_params_ecdsa_with postcondition Unknown \old(len) ≢ 0 ⇒ \result < 0 -src x509-parser.c 1715 parse_algoid_params_ecdsa_with ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 1821 find_curve_by_oid precondition Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1822 find_curve_by_oid postcondition Unknown \result ≢ (_curve const *)0 ⇒ (∃ ℤ i; 0 ≤ i < sizeof(known_curves) / sizeof(known_curves[0]) ∧ \result ≡ known_curves[i]) src x509-parser.c 1853 find_curve_by_oid user assertion Unknown \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1870 parse_algoid_params_ecPublicKey precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1873 parse_algoid_params_ecPublicKey postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 src x509-parser.c 1875 parse_algoid_params_ecPublicKey postcondition Unknown \result ≡ 0 ⇒ (∃ ℤ i; 0 ≤ i < sizeof(known_curves) / sizeof(known_curves[0]) ∧ \old(param)->curve_param ≡ known_curves[i]) -src x509-parser.c 1884 parse_algoid_params_ecPublicKey ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 1922 parse_algoid_params_ecPublicKey precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1936 parse_algoid_params_ecPublicKey precondition of find_curve_by_oid Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1976 parse_subjectpubkey_ec precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 1979 parse_subjectpubkey_ec postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 1992 parse_subjectpubkey_ec ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 1999 parse_subjectpubkey_ec precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2024 parse_subjectpubkey_ec mem_access Unknown \valid_read(buf + 0) src x509-parser.c 2046 parse_subjectpubkey_ec mem_access Unknown \valid_read(buf + 0) src x509-parser.c 2105 parse_algoid_params_generic precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2107 parse_algoid_params_generic postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2118 parse_algoid_params_generic ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2133 parse_algoid_params_rsa precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2135 parse_algoid_params_rsa postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2146 parse_algoid_params_rsa ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2166 parse_algoid_params_rsa precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) src x509-parser.c 2197 parse_subjectpubkey_rsa precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2200 parse_subjectpubkey_rsa postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2212 parse_subjectpubkey_rsa ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2225 parse_subjectpubkey_rsa precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2250 parse_subjectpubkey_rsa mem_access Unknown \valid_read(buf + 0) src x509-parser.c 2262 parse_subjectpubkey_rsa precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2273 parse_subjectpubkey_rsa precondition of parse_integer Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 2280 parse_subjectpubkey_rsa unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) src x509-parser.c 2284 parse_subjectpubkey_rsa precondition of parse_integer Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 2291 parse_subjectpubkey_rsa unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) src x509-parser.c 2309 find_alg_by_oid precondition Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2310 find_alg_by_oid postcondition Unknown \result ≢ (_alg_id const *)0 ⇒ (∃ ℤ i; 0 ≤ i < sizeof(known_algs) / sizeof(known_algs[0]) ∧ \result ≡ known_algs[i]) src x509-parser.c 2311 find_alg_by_oid postcondition Unknown \old(len) ≡ 0 ⇒ \result ≡ (_alg_id const *)0 -src x509-parser.c 2321 find_alg_by_oid ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2341 find_alg_by_oid user assertion Unknown \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2363 parse_x509_AlgorithmIdentifier precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2368 parse_x509_AlgorithmIdentifier postcondition Unknown \result ≡ 0 ⇒ (∃ unsigned char x; *\old(alg) ≡ known_algs[x]) src x509-parser.c 2369 parse_x509_AlgorithmIdentifier postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 2370 parse_x509_AlgorithmIdentifier postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2386 parse_x509_AlgorithmIdentifier ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2393 parse_x509_AlgorithmIdentifier precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2403 parse_x509_AlgorithmIdentifier precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2410 parse_x509_AlgorithmIdentifier precondition of find_alg_by_oid Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 2419 parse_x509_AlgorithmIdentifier unsigned_downcast Unknown 0 ≤ (int)((int)data_len - (int)oid_len) src x509-parser.c 2423 parse_x509_AlgorithmIdentifier precondition of parse_algoid_params_ecPublicKey Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2423 parse_x509_AlgorithmIdentifier precondition of parse_algoid_params_ecdsa_with Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2423 parse_x509_AlgorithmIdentifier precondition of parse_algoid_params_generic Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2423 parse_x509_AlgorithmIdentifier precondition of parse_algoid_params_rsa Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 2430 parse_x509_AlgorithmIdentifier unsigned_downcast Unknown (int)((int)hdr_len + (int)data_len) ≤ 65535 src x509-parser.c 2463 check_utf8_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2465 check_utf8_string postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2474 check_utf8_string ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2481 check_utf8_string loop invariant Unknown \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2486 check_utf8_string mem_access Unknown \valid_read(buf + 0) src x509-parser.c 2511 check_utf8_string user assertion Unknown \valid_read(buf + (0 .. 1)) @@ -153,7 +146,6 @@ src x509-parser.c 2648 check_printable_string loop invariant Unknown 0 ≤ rbyte src x509-parser.c 2653 check_printable_string mem_access Unknown \valid_read(buf + rbytes) src x509-parser.c 2695 check_visible_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2697 check_visible_string postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2707 check_visible_string ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2718 check_visible_string mem_access Unknown \valid_read(buf + rbytes) src x509-parser.c 2780 check_teletex_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2795 check_universal_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -161,7 +153,6 @@ src x509-parser.c 2810 check_bmp_string precondition Unknown len > 0 ∧ buf ≢ src x509-parser.c 2854 parse_directory_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2856 parse_directory_string postcondition Unknown \result ≡ 0 ⇒ \old(len) ≥ 2 ∧ \old(lb) ≤ \old(len) - 2 ≤ \old(ub) src x509-parser.c 2857 parse_directory_string postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2866 parse_directory_string ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2878 parse_directory_string mem_access Unknown \valid_read(buf + 0) src x509-parser.c 2881 parse_directory_string mem_access Unknown \valid_read(buf + 1) src x509-parser.c 2896 parse_directory_string precondition of check_printable_string Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -172,13 +163,11 @@ src x509-parser.c 2926 parse_directory_string precondition of check_bmp_string U src x509-parser.c 2955 parse_printable_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 2957 parse_printable_string postcondition Unknown \result ≡ 0 ⇒ \old(len) ≥ 2 ∧ \old(lb) ≤ \old(len) - 2 ≤ \old(ub) src x509-parser.c 2958 parse_printable_string postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 2967 parse_printable_string ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 2979 parse_printable_string mem_access Unknown \valid_read(buf + 0) src x509-parser.c 2987 parse_printable_string mem_access Unknown \valid_read(buf + 1) src x509-parser.c 3000 parse_printable_string precondition of check_printable_string Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3014 check_ia5_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3016 check_ia5_string postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 3025 check_ia5_string ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 3032 check_ia5_string loop invariant Unknown ∀ ℤ x; 0 ≤ x < i ⇒ *(buf + x) ≤ 0x7f src x509-parser.c 3038 check_ia5_string mem_access Unknown \valid_read(buf + i) src x509-parser.c 3057 parse_ia5_string precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -217,9 +206,10 @@ src x509-parser.c 3257 parse_rdn_val_dn_qual postcondition Unknown \old(len) ≡ src x509-parser.c 3267 parse_rdn_val_dn_qual precondition of parse_printable_string Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3310 parse_rdn_val_dc precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3312 parse_rdn_val_dc postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 3322 parse_rdn_val_dc ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 3329 parse_rdn_val_dc precondition of parse_ia5_string Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 3336 parse_rdn_val_dc unsigned_downcast Unknown 0 ≤ (int)((int)len - 2) src x509-parser.c 3339 parse_rdn_val_dc mem_access Unknown \valid_read(buf + 0) +src x509-parser.c 3348 parse_rdn_val_dc unsigned_downcast Unknown 0 ≤ (int)((int)len - 1) src x509-parser.c 3356 parse_rdn_val_dc mem_access Unknown \valid_read(buf + (int)((int)len - 1)) src x509-parser.c 3369 parse_rdn_val_dc loop invariant Unknown 0 ≤ i ≤ len src x509-parser.c 3374 parse_rdn_val_dc mem_access Unknown \valid_read(buf + i) @@ -229,14 +219,15 @@ src x509-parser.c 3400 parse_rdn_val_pseudo precondition of parse_directory_stri src x509-parser.c 3481 find_dn_by_oid precondition Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3482 find_dn_by_oid postcondition Unknown \result ≢ (_name_oid const *)0 ⇒ (∃ ℤ i; 0 ≤ i < sizeof(known_dn_oids) / sizeof(known_dn_oids[0]) ∧ \result ≡ &known_dn_oids[i]) src x509-parser.c 3483 find_dn_by_oid postcondition Unknown \old(len) ≡ 0 ⇒ \result ≡ (_name_oid const *)0 -src x509-parser.c 3493 find_dn_by_oid ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 3513 find_dn_by_oid user assertion Unknown \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3536 parse_AttributeTypeAndValue precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3539 parse_AttributeTypeAndValue postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 3560 parse_AttributeTypeAndValue precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3568 parse_AttributeTypeAndValue user assertion Unknown parsed ≤ len +src x509-parser.c 3571 parse_AttributeTypeAndValue unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)hdr_len) src x509-parser.c 3574 parse_AttributeTypeAndValue precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3580 parse_AttributeTypeAndValue precondition of find_dn_by_oid Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 3587 parse_AttributeTypeAndValue unsigned_downcast Unknown 0 ≤ (int)((int)data_len - (int)oid_len) src x509-parser.c 3601 parse_AttributeTypeAndValue precondition of parse_rdn_val_cn Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3601 parse_AttributeTypeAndValue precondition of parse_rdn_val_country Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3601 parse_AttributeTypeAndValue precondition of parse_rdn_val_dc Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -255,13 +246,14 @@ src x509-parser.c 3627 parse_RelativeDistinguishedName postcondition Unknown \re src x509-parser.c 3646 parse_RelativeDistinguishedName precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3659 parse_RelativeDistinguishedName loop invariant Unknown \valid_read(buf + (0 .. rdn_remain - 1)) src x509-parser.c 3665 parse_RelativeDistinguishedName precondition of parse_AttributeTypeAndValue Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 3676 parse_RelativeDistinguishedName unsigned_downcast Unknown 0 ≤ (int)((int)rdn_remain - (int)parsed) src x509-parser.c 3756 parse_x509_Name precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3760 parse_x509_Name postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 3762 parse_x509_Name postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 3773 parse_x509_Name ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 3780 parse_x509_Name precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 3792 parse_x509_Name loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 3798 parse_x509_Name precondition of parse_RelativeDistinguishedName Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 3805 parse_x509_Name unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 3819 compute_decimal precondition Unknown 0x30 ≤ d ≤ 0x39 src x509-parser.c 3820 compute_decimal precondition Unknown 0x30 ≤ u ≤ 0x39 src x509-parser.c 3832 parse_UTCTime precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -310,86 +302,97 @@ src x509-parser.c 4097 parse_generalizedTime precondition of compute_decimal Unk src x509-parser.c 4143 parse_Time precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4154 parse_Time postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 4155 parse_Time postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 4166 parse_Time ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 4177 parse_Time mem_access Unknown \valid_read(buf + 0) src x509-parser.c 4181 parse_Time precondition of parse_UTCTime Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4188 parse_Time precondition of parse_generalizedTime Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4249 parse_x509_Validity precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4253 parse_x509_Validity postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 4254 parse_x509_Validity postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 4269 parse_x509_Validity ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 4276 parse_x509_Validity precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4287 parse_x509_Validity precondition of parse_Time Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 4301 parse_x509_Validity unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)nb_len) src x509-parser.c 4305 parse_x509_Validity precondition of parse_Time Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 4319 parse_x509_Validity unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)na_len) src x509-parser.c 4377 parse_x509_subjectPublicKeyInfo precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4381 parse_x509_subjectPublicKeyInfo postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 4382 parse_x509_subjectPublicKeyInfo postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 4393 parse_x509_subjectPublicKeyInfo ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 4400 parse_x509_subjectPublicKeyInfo precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4416 parse_x509_subjectPublicKeyInfo precondition of parse_x509_AlgorithmIdentifier Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4423 parse_x509_subjectPublicKeyInfo mem_access Unknown \valid_read(&alg->alg_type) +src x509-parser.c 4430 parse_x509_subjectPublicKeyInfo unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 4443 parse_x509_subjectPublicKeyInfo precondition of parse_subjectpubkey_ec Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4443 parse_x509_subjectPublicKeyInfo precondition of parse_subjectpubkey_rsa Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4569 parse_GeneralName precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4573 parse_GeneralName postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 4574 parse_GeneralName postcondition Unknown \result ≡ 0 ⇒ 0 ≤ *\old(empty) ≤ 1 src x509-parser.c 4575 parse_GeneralName postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 4585 parse_GeneralName ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 4603 parse_GeneralName mem_access Unknown \valid_read(buf + 0) src x509-parser.c 4617 parse_GeneralName precondition of get_length Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 4623 parse_GeneralName unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)grabbed) src x509-parser.c 4631 parse_GeneralName precondition of check_ia5_string Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 4663 parse_GeneralName unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)name_len) src x509-parser.c 4667 parse_GeneralName user assertion Unknown *eaten > 1 src x509-parser.c 4674 parse_GeneralName precondition of get_length Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 4680 parse_GeneralName unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)grabbed) +src x509-parser.c 4690 parse_GeneralName unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)name_len) src x509-parser.c 4694 parse_GeneralName user assertion Unknown *eaten > 1 src x509-parser.c 4712 parse_GeneralName precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4722 parse_GeneralName precondition of parse_x509_Name Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 4729 parse_GeneralName unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)grabbed) src x509-parser.c 4738 parse_GeneralName user assertion Unknown *eaten > 1 src x509-parser.c 4772 parse_GeneralNames precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4776 parse_GeneralNames postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 4777 parse_GeneralNames postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 4787 parse_GeneralNames ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 4793 parse_GeneralNames precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4805 parse_GeneralNames loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 4809 parse_GeneralNames precondition of parse_GeneralName Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 4815 parse_GeneralNames unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 4829 parse_AccessDescription precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4832 parse_AccessDescription postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 4855 parse_AccessDescription precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4864 parse_AccessDescription user assertion Unknown saved_ad_len ≤ len +src x509-parser.c 4865 parse_AccessDescription unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 4866 parse_AccessDescription user assertion Unknown remain ≥ data_len src x509-parser.c 4870 parse_AccessDescription precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4883 parse_AccessDescription precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) src x509-parser.c 4887 parse_AccessDescription precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) +src x509-parser.c 4897 parse_AccessDescription unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)oid_len) +src x509-parser.c 4898 parse_AccessDescription unsigned_downcast Unknown 0 ≤ (int)((int)data_len - (int)oid_len) src x509-parser.c 4899 parse_AccessDescription user assertion Unknown remain ≥ data_len src x509-parser.c 4902 parse_AccessDescription precondition of parse_GeneralName Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4915 parse_AccessDescription user assertion Unknown remain ≥ data_len ≥ al_len +src x509-parser.c 4916 parse_AccessDescription unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)al_len) +src x509-parser.c 4917 parse_AccessDescription unsigned_downcast Unknown 0 ≤ (int)((int)data_len - (int)al_len) src x509-parser.c 4926 parse_AccessDescription user assertion Unknown *eaten ≤ len src x509-parser.c 4982 parse_ext_AIA precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 4986 parse_ext_AIA postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 4996 parse_ext_AIA ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 5015 parse_ext_AIA precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5023 parse_ext_AIA unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 5049 parse_ext_AIA loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 5055 parse_ext_AIA precondition of parse_AccessDescription Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5062 parse_ext_AIA unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 5088 parse_ext_AKI precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5092 parse_ext_AKI postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 5104 parse_ext_AKI ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 5121 parse_ext_AKI precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5145 parse_ext_AKI precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5156 parse_ext_AKI unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)((int)key_id_hdr_len + (int)key_id_data_len)) src x509-parser.c 5165 parse_ext_AKI precondition of parse_GeneralNames Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5171 parse_ext_AKI unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 5174 parse_ext_AKI precondition of parse_CertificateSerialNumber Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5183 parse_ext_AKI unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)cert_serial_len) src x509-parser.c 5208 parse_ext_SKI precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5212 parse_ext_SKI postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 5222 parse_ext_SKI ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 5240 parse_ext_SKI precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5260 parse_ext_SKI unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)((int)key_id_hdr_len + (int)key_id_data_len)) src x509-parser.c 5290 parse_nine_bit_named_bit_list precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5293 parse_nine_bit_named_bit_list postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 5307 parse_nine_bit_named_bit_list ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 5314 parse_nine_bit_named_bit_list mem_access Unknown \valid_read(buf + 0) src x509-parser.c 5360 parse_nine_bit_named_bit_list mem_access Unknown \valid_read(buf + 1) src x509-parser.c 5424 parse_nine_bit_named_bit_list mem_access Unknown \valid_read(buf + 2) src x509-parser.c 5495 parse_ext_keyUsage precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5499 parse_ext_keyUsage postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 5510 parse_ext_keyUsage ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 5524 parse_ext_keyUsage precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5538 parse_ext_keyUsage unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)hdr_len) src x509-parser.c 5545 parse_ext_keyUsage precondition of parse_nine_bit_named_bit_list Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5586 parse_CPSuri precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5590 parse_CPSuri postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) @@ -398,7 +401,6 @@ src x509-parser.c 5605 parse_CPSuri precondition of parse_ia5_string Unknown len src x509-parser.c 5628 parse_DisplayText precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5632 parse_DisplayText postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 5633 parse_DisplayText postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 5643 parse_DisplayText ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 5649 parse_DisplayText mem_access Unknown \valid_read(buf + 0) src x509-parser.c 5656 parse_DisplayText precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5667 parse_DisplayText precondition of check_utf8_string Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -408,149 +410,174 @@ src x509-parser.c 5688 parse_DisplayText precondition of check_bmp_string Unknow src x509-parser.c 5729 parse_NoticeReference precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5733 parse_NoticeReference postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 5734 parse_NoticeReference postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 5743 parse_NoticeReference ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 5752 parse_NoticeReference precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5767 parse_NoticeReference precondition of parse_DisplayText Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5773 parse_NoticeReference unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 5780 parse_NoticeReference precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5787 parse_NoticeReference unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 5800 parse_NoticeReference loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 5805 parse_NoticeReference precondition of parse_integer Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5813 parse_NoticeReference unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 5843 parse_UserNotice precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5847 parse_UserNotice postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 5848 parse_UserNotice postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 src x509-parser.c 5866 parse_UserNotice precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5873 parse_UserNotice unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 5884 parse_UserNotice precondition of parse_NoticeReference Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5886 parse_UserNotice unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 5891 parse_UserNotice precondition of parse_DisplayText Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5893 parse_UserNotice unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 5926 parse_policyQualifierInfo precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5930 parse_policyQualifierInfo postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 5951 parse_policyQualifierInfo precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5965 parse_policyQualifierInfo precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 5972 parse_policyQualifierInfo precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) +src x509-parser.c 5976 parse_policyQualifierInfo unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)oid_len) src x509-parser.c 5978 parse_policyQualifierInfo precondition of parse_CPSuri Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 5984 parse_policyQualifierInfo unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)cpsuri_len) src x509-parser.c 5988 parse_policyQualifierInfo precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) +src x509-parser.c 5992 parse_policyQualifierInfo unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)oid_len) src x509-parser.c 5994 parse_policyQualifierInfo precondition of parse_UserNotice Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6000 parse_policyQualifierInfo unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)cpsunotice_len) src x509-parser.c 6025 parse_PolicyInformation precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6029 parse_PolicyInformation postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 6045 parse_PolicyInformation precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6058 parse_PolicyInformation precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6064 parse_PolicyInformation unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)oid_len) src x509-parser.c 6070 parse_PolicyInformation precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6078 parse_PolicyInformation unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 6094 parse_PolicyInformation loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 6100 parse_PolicyInformation precondition of parse_policyQualifierInfo Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6106 parse_PolicyInformation unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)pqi_len) src x509-parser.c 6176 parse_ext_certPolicies precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6180 parse_ext_certPolicies postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6191 parse_ext_certPolicies ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6213 parse_ext_certPolicies precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6232 parse_ext_certPolicies loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 6236 parse_ext_certPolicies precondition of parse_PolicyInformation Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6242 parse_ext_certPolicies unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) src x509-parser.c 6266 parse_ext_policyMapping precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6270 parse_ext_policyMapping postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6280 parse_ext_policyMapping ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6297 parse_ext_policyMapping precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6316 parse_ext_policyMapping loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 6320 parse_ext_policyMapping precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6329 parse_ext_policyMapping unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 6332 parse_ext_policyMapping precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6339 parse_ext_policyMapping unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) +src x509-parser.c 6340 parse_ext_policyMapping unsigned_downcast Unknown 0 ≤ (int)((int)data_len - (int)eaten) src x509-parser.c 6343 parse_ext_policyMapping precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6349 parse_ext_policyMapping unsigned_downcast Unknown 0 ≤ (int)((int)data_len - (int)eaten) +src x509-parser.c 6361 parse_ext_policyMapping unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) src x509-parser.c 6401 parse_ext_SAN precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6405 parse_ext_SAN postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6414 parse_ext_SAN ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6421 parse_ext_SAN precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6451 parse_ext_SAN loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 6456 parse_ext_SAN precondition of parse_GeneralName Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6484 parse_ext_SAN mem_access Unknown \valid_read(buf + 0) +src x509-parser.c 6498 parse_ext_SAN unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) src x509-parser.c 6518 parse_ext_IAN precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6522 parse_ext_IAN postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6532 parse_ext_IAN ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6546 parse_ext_IAN precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6582 parse_ext_IAN loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 6586 parse_ext_IAN precondition of parse_GeneralName Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6592 parse_ext_IAN unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) src x509-parser.c 6622 parse_ext_subjectDirAttr precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6626 parse_ext_subjectDirAttr postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6636 parse_ext_subjectDirAttr ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6653 parse_ext_subjectDirAttr precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6671 parse_ext_subjectDirAttr loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 6676 parse_ext_subjectDirAttr precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6685 parse_ext_subjectDirAttr unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 6688 parse_ext_subjectDirAttr precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6696 parse_ext_subjectDirAttr unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)data_len) src x509-parser.c 6717 parse_ext_basicConstraints precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6721 parse_ext_basicConstraints postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6733 parse_ext_basicConstraints ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6743 parse_ext_basicConstraints precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6782 parse_ext_basicConstraints precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) src x509-parser.c 6791 parse_ext_basicConstraints precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) src x509-parser.c 6804 parse_ext_basicConstraints mem_access Unknown \valid_read(buf + 5) src x509-parser.c 6837 parse_GeneralSubtrees precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6839 parse_GeneralSubtrees postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6848 parse_GeneralSubtrees ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6854 parse_GeneralSubtrees precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6865 parse_GeneralSubtrees precondition of parse_GeneralName Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6872 parse_GeneralSubtrees unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)grabbed) src x509-parser.c 6885 parse_GeneralSubtrees precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6894 parse_GeneralSubtrees precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6918 parse_ext_nameConstraints precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6922 parse_ext_nameConstraints postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 6932 parse_ext_nameConstraints ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 6949 parse_ext_nameConstraints precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 6969 parse_ext_nameConstraints precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6973 parse_ext_nameConstraints unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 6975 parse_ext_nameConstraints precondition of parse_GeneralSubtrees Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6982 parse_ext_nameConstraints unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)data_len) src x509-parser.c 6986 parse_ext_nameConstraints precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6990 parse_ext_nameConstraints unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 6992 parse_ext_nameConstraints precondition of parse_GeneralSubtrees Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 6999 parse_ext_nameConstraints unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)data_len) src x509-parser.c 7030 parse_ext_policyConstraints precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7034 parse_ext_policyConstraints postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 7044 parse_ext_policyConstraints ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 7061 parse_ext_policyConstraints precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7083 parse_ext_policyConstraints precondition of parse_integer Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7098 parse_ext_policyConstraints unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 7102 parse_ext_policyConstraints precondition of parse_integer Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7117 parse_ext_policyConstraints unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 7188 find_kp_by_oid precondition Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7189 find_kp_by_oid postcondition Unknown \result ≢ (_kp_oid const *)0 ⇒ (∃ ℤ i; 0 ≤ i < sizeof(known_kp_oids) / sizeof(known_kp_oids[0]) ∧ \result ≡ &known_kp_oids[i]) src x509-parser.c 7190 find_kp_by_oid postcondition Unknown \old(len) ≡ 0 ⇒ \result ≡ (_kp_oid const *)0 -src x509-parser.c 7200 find_kp_by_oid ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 7220 find_kp_by_oid user assertion Unknown \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7244 parse_ext_EKU precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7248 parse_ext_EKU postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 7259 parse_ext_EKU ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 7265 parse_ext_EKU precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7285 parse_ext_EKU loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 7289 parse_ext_EKU precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7295 parse_ext_EKU precondition of find_kp_by_oid Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7314 parse_ext_EKU unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)oid_len) src x509-parser.c 7338 parse_crldp_reasons precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7342 parse_crldp_reasons postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 7343 parse_crldp_reasons postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 7352 parse_crldp_reasons ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 7358 parse_crldp_reasons precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7366 parse_crldp_reasons unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)hdr_len) src x509-parser.c 7368 parse_crldp_reasons precondition of parse_nine_bit_named_bit_list Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7405 parse_DistributionPoint precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7410 parse_DistributionPoint postcondition Unknown \result ≡ 0 ⇒ 0 < *\old(eaten) ≤ \old(len) src x509-parser.c 7430 parse_DistributionPoint precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7439 parse_DistributionPoint user assertion Unknown total_len > 0 src x509-parser.c 7447 parse_DistributionPoint precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7454 parse_DistributionPoint unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)hdr_len) src x509-parser.c 7462 parse_DistributionPoint mem_access Unknown \valid_read(buf + 0) src x509-parser.c 7470 parse_DistributionPoint precondition of parse_GeneralNames Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7478 parse_DistributionPoint unsigned_downcast Unknown 0 ≤ (int)((int)dpn_remain - (int)dpn_eaten) +src x509-parser.c 7509 parse_DistributionPoint unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)data_len) src x509-parser.c 7513 parse_DistributionPoint precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7516 parse_DistributionPoint precondition of parse_crldp_reasons Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7523 parse_DistributionPoint unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 7534 parse_DistributionPoint precondition of parse_GeneralNames Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7541 parse_DistributionPoint unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 7587 parse_ext_CRLDP precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7591 parse_ext_CRLDP postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 7601 parse_ext_CRLDP ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 7615 parse_ext_CRLDP precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7638 parse_ext_CRLDP loop invariant Unknown \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 7644 parse_ext_CRLDP precondition of parse_DistributionPoint Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 7650 parse_ext_CRLDP unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)eaten) src x509-parser.c 7669 parse_ext_inhibitAnyPolicy precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7673 parse_ext_inhibitAnyPolicy postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 7684 parse_ext_inhibitAnyPolicy ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 7700 parse_ext_inhibitAnyPolicy precondition of parse_integer Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 7718 parse_ext_inhibitAnyPolicy mem_access Unknown \valid_read(buf + 2) src x509-parser.c 7759 parse_ext_bad_oid precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) -src x509-parser.c 7770 parse_ext_bad_oid ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 8059 find_ext_by_oid precondition Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8060 find_ext_by_oid postcondition Unknown \result ≢ (_ext_oid const *)0 ⇒ (∃ ℤ i; 0 ≤ i < sizeof(known_ext_oids) / sizeof(known_ext_oids[0]) ∧ \result ≡ &known_ext_oids[i]) src x509-parser.c 8061 find_ext_by_oid postcondition Unknown \old(len) ≡ 0 ⇒ \result ≡ (_ext_oid const *)0 -src x509-parser.c 8071 find_ext_by_oid ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 8091 find_ext_by_oid user assertion Unknown \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8169 parse_x509_Extension precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8175 parse_x509_Extension postcondition Unknown \result ≡ 0 ⇒ 1 ≤ *\old(eaten) ≤ \old(len) src x509-parser.c 8196 parse_x509_Extension precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8205 parse_x509_Extension unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)ext_hdr_len) src x509-parser.c 8214 parse_x509_Extension precondition of parse_OID Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8222 parse_x509_Extension precondition of find_ext_by_oid Unknown len > 0 ∧ buf ≢ (u8 const *)0 ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8257 parse_x509_Extension unsigned_downcast Unknown 0 ≤ (int)((int)ext_data_len - (int)oid_len) src x509-parser.c 8266 parse_x509_Extension precondition of parse_boolean Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8274 parse_x509_Extension mem_access Unknown \valid_read(buf + 2) +src x509-parser.c 8287 parse_x509_Extension unsigned_downcast Unknown 0 ≤ (int)((int)ext_data_len - (int)parsed) src x509-parser.c 8294 parse_x509_Extension precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8303 parse_x509_Extension unsigned_downcast Unknown 0 ≤ (int)((int)ext_data_len - (int)hdr_len) src x509-parser.c 8314 parse_x509_Extension precondition of parse_ext_AIA Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8314 parse_x509_Extension precondition of parse_ext_AKI Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8314 parse_x509_Extension precondition of parse_ext_CRLDP Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) @@ -571,51 +598,69 @@ src x509-parser.c 8345 parse_x509_Extensions precondition Unknown len > 0 ∧ bu src x509-parser.c 8350 parse_x509_Extensions postcondition Unknown \result ≡ 0 ⇒ 1 ≤ *\old(eaten) ≤ \old(len) src x509-parser.c 8375 parse_x509_Extensions precondition of parse_explicit_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8385 parse_x509_Extensions user assertion Unknown \valid_read(buf + (0 .. remain - 1)) +src x509-parser.c 8387 parse_x509_Extensions unsigned_downcast Unknown (int)((int)hdr_len + (int)data_len) ≤ 65535 src x509-parser.c 8388 parse_x509_Extensions user assertion Unknown saved_len ≤ len src x509-parser.c 8389 parse_x509_Extensions user assertion Unknown data_len ≤ saved_len src x509-parser.c 8412 parse_x509_Extensions loop invariant Unknown remain ≢ 0 ⇒ \valid_read(buf + (0 .. remain - 1)) src x509-parser.c 8418 parse_x509_Extensions precondition of parse_x509_Extension Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8425 parse_x509_Extensions unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)ext_len) src x509-parser.c 8447 parse_x509_Extensions user assertion Unknown 1 ≤ saved_len ≤ len src x509-parser.c 8482 parse_x509_tbsCertificate precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8486 parse_x509_tbsCertificate postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 src x509-parser.c 8488 parse_x509_tbsCertificate postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 8538 parse_x509_tbsCertificate precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8554 parse_x509_tbsCertificate precondition of parse_x509_Version Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8561 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8564 parse_x509_tbsCertificate precondition of parse_CertificateSerialNumber Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8573 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8576 parse_x509_tbsCertificate precondition of parse_x509_AlgorithmIdentifier Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8582 parse_x509_tbsCertificate mem_access Unknown \valid_read(&alg->alg_type) +src x509-parser.c 8589 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8592 parse_x509_tbsCertificate precondition of parse_x509_Name Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8613 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8616 parse_x509_tbsCertificate precondition of parse_x509_Validity Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8623 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8626 parse_x509_tbsCertificate precondition of parse_x509_Name Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8636 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8644 parse_x509_tbsCertificate precondition of bufs_differ Unknown \valid_read(b1 + (0 .. n - 1)) src x509-parser.c 8644 parse_x509_tbsCertificate precondition of bufs_differ Unknown \valid_read(b2 + (0 .. n - 1)) src x509-parser.c 8648 parse_x509_tbsCertificate precondition of parse_x509_subjectPublicKeyInfo Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8655 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8687 parse_x509_tbsCertificate precondition of parse_x509_Extensions Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8694 parse_x509_tbsCertificate unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)parsed) src x509-parser.c 8800 parse_x509_tbsCertificate user assertion Unknown 1 < tbs_hdr_len + tbs_data_len ≤ len +src x509-parser.c 8801 parse_x509_tbsCertificate unsigned_downcast Unknown (int)((int)tbs_hdr_len + (int)tbs_data_len) ≤ 65535 src x509-parser.c 8812 parse_x509_signatureAlgorithm precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8816 parse_x509_signatureAlgorithm postcondition Unknown \result ≡ 0 ⇒ 1 < *\old(eaten) ≤ \old(len) src x509-parser.c 8817 parse_x509_signatureAlgorithm postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 8829 parse_x509_signatureAlgorithm ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 8836 parse_x509_signatureAlgorithm precondition of parse_x509_AlgorithmIdentifier Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8842 parse_x509_signatureAlgorithm mem_access Unknown \valid_read(&alg->alg_type) +src x509-parser.c 8849 parse_x509_signatureAlgorithm unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)parsed) src x509-parser.c 8874 parse_sig_generic precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8878 parse_sig_generic postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 8888 parse_sig_generic precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8906 parse_sig_generic unsigned_downcast Unknown (int)((int)bs_hdr_len + (int)bs_data_len) ≤ 65535 src x509-parser.c 8917 parse_sig_ecdsa precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 8921 parse_sig_ecdsa postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 8938 parse_sig_ecdsa precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 8945 parse_sig_ecdsa unsigned_downcast Unknown (int)((int)bs_hdr_len + (int)bs_data_len) ≤ 65535 src x509-parser.c 8946 parse_sig_ecdsa user assertion Unknown saved_sig_len ≤ len src x509-parser.c 8983 parse_sig_ecdsa mem_access Unknown \valid_read(buf + 0) src x509-parser.c 8995 parse_sig_ecdsa precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 9003 parse_sig_ecdsa unsigned_downcast Unknown 0 ≤ (int)((int)sig_len - (int)hdr_len) src x509-parser.c 9007 parse_sig_ecdsa precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 9014 parse_sig_ecdsa unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)((int)hdr_len + (int)data_len)) src x509-parser.c 9018 parse_sig_ecdsa precondition of parse_id_len Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 9025 parse_sig_ecdsa unsigned_downcast Unknown 0 ≤ (int)((int)remain - (int)((int)hdr_len + (int)data_len)) src x509-parser.c 9050 parse_x509_signatureValue precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 9054 parse_x509_signatureValue postcondition Unknown \result ≡ 0 ⇒ *\old(eaten) ≤ \old(len) src x509-parser.c 9055 parse_x509_signatureValue postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 -src x509-parser.c 9064 parse_x509_signatureValue ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0) src x509-parser.c 9083 parse_x509_signatureValue precondition of parse_sig_ecdsa Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 9083 parse_x509_signatureValue precondition of parse_sig_generic Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) src x509-parser.c 9099 parse_x509_cert postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0 +src x509-parser.c 9126 parse_x509_cert unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)eaten) src x509-parser.c 9140 parse_x509_cert precondition of parse_x509_tbsCertificate Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 9146 parse_x509_cert unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)eaten) src x509-parser.c 9150 parse_x509_cert precondition of parse_x509_signatureAlgorithm Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) +src x509-parser.c 9156 parse_x509_cert unsigned_downcast Unknown 0 ≤ (int)((int)len - (int)eaten) src x509-parser.c 9160 parse_x509_cert precondition of parse_x509_signatureValue Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1)) diff --git a/x509-parser/.frama-c/x509-parser.wp/alarms.csv b/x509-parser/.frama-c/x509-parser.wp/alarms.csv new file mode 100644 index 0000000000000000000000000000000000000000..81ffdf915f631877c7f27e533caa86d678b5a603 --- /dev/null +++ b/x509-parser/.frama-c/x509-parser.wp/alarms.csv @@ -0,0 +1,30 @@ +directory file line function property kind status property +src x509-parser.c 3819 compute_decimal precondition Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 3820 compute_decimal precondition Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 3927 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 3927 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 3934 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 3935 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 3935 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 3936 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 3936 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 3937 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 3937 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 3938 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 3938 parse_UTCTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 3976 compute_year precondition Unknown 0x30 ≤ d1 ≤ 0x39 +src x509-parser.c 3977 compute_year precondition Unknown 0x30 ≤ d2 ≤ 0x39 +src x509-parser.c 3979 compute_year precondition Unknown 0x30 ≤ d4 ≤ 0x39 +src x509-parser.c 4092 parse_generalizedTime precondition of compute_year Unknown 0x30 ≤ d1 ≤ 0x39 +src x509-parser.c 4092 parse_generalizedTime precondition of compute_year Unknown 0x30 ≤ d2 ≤ 0x39 +src x509-parser.c 4092 parse_generalizedTime precondition of compute_year Unknown 0x30 ≤ d4 ≤ 0x39 +src x509-parser.c 4093 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 4093 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 4094 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 4094 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 4095 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 4095 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 4096 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 4096 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 +src x509-parser.c 4097 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ d ≤ 0x39 +src x509-parser.c 4097 parse_generalizedTime precondition of compute_decimal Unknown 0x30 ≤ u ≤ 0x39 diff --git a/x509-parser/.frama-c/x509-parser.wp/warnings.log b/x509-parser/.frama-c/x509-parser.wp/warnings.log new file mode 100644 index 0000000000000000000000000000000000000000..320c18207f5fc047b31d173626a05773f9b3b35a --- /dev/null +++ b/x509-parser/.frama-c/x509-parser.wp/warnings.log @@ -0,0 +1,111 @@ +[kernel] warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration. +[wp] warning: Missing RTE guards +src/x509-parser.c:9051:[wp] warning: \valid_function not yet implemented +(\valid_function(sig_alg->parse_sig)) +src/x509-parser.c:9238:[wp] warning: Cast with incompatible pointers types (source: uint8*) (target: sint8*) +FRAMAC_SHARE/libc/__fc_builtin.h:38:[wp] warning: Memory model hypotheses for function 'Frama_C_make_unknown': +/*@ + behavior wp_typed: + requires \separated(p + (..), &Frama_C_entropy_source); + requires \separated(p + (0 .. l - 1), &Frama_C_entropy_source); + */ +extern void Frama_C_make_unknown(char *p, size_t l); +src/x509-parser.c:9232:[wp:pedantic-assigns] warning: No 'assigns' specification for function 'main'. +Callers assumptions might be imprecise. +src/x509-parser.c:1876:[wp:pedantic-assigns] warning: No \from specification for assigned pointer 'param->curve_param'. +Callers assumptions might be imprecise. +src/x509-parser.c:1878:[wp] warning: Memory model hypotheses for function 'parse_algoid_params_ecPublicKey': +/*@ + behavior wp_typed: + requires + \separated((_curve const **)known_curves + (..), ¶m->curve_param); + requires \separated(buf + (..), (_curve const **)known_curves + (..)); + requires \separated(param, (_curve const **)known_curves + (..)); + ensures + \separated((_curve const **)known_curves + (..), ¶m->curve_param); + */ +static int parse_algoid_params_ecPublicKey(u8 const *buf, u16 len, + alg_param *param); +src/x509-parser.c:2140:[wp:pedantic-assigns] warning: No \from specification for assigned pointer 'param->null_param'. +Callers assumptions might be imprecise. +src/x509-parser.c:1827:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_curve_by_oid'returning pointer type. +Callers assumptions might be imprecise. +src/x509-parser.c:1827:[wp] warning: Memory model hypotheses for function 'find_curve_by_oid': +/*@ + behavior wp_typed: + requires \separated(buf + (..), (_curve const **)known_curves + (..)); + ensures \separated(\result, (_curve const **)known_curves + (..)); + */ +static _curve const *find_curve_by_oid(u8 const *buf, u16 len); +src/x509-parser.c:2315:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_alg_by_oid'returning pointer type. +Callers assumptions might be imprecise. +src/x509-parser.c:2315:[wp] warning: Memory model hypotheses for function 'find_alg_by_oid': +/*@ + behavior wp_typed: + requires \separated(buf + (..), (_alg_id const **)known_algs + (..)); + ensures \separated(\result, (_alg_id const **)known_algs + (..)); + */ +static _alg_id const *find_alg_by_oid(u8 const *buf, u16 len); +src/x509-parser.c:2373:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*alg'. +Callers assumptions might be imprecise. +src/x509-parser.c:2375:[wp] warning: Memory model hypotheses for function 'parse_x509_AlgorithmIdentifier': +/*@ + behavior wp_typed: + requires \separated(buf + (..), (_alg_id const **)known_algs + (..)); + requires \separated(param + (..), (_alg_id const **)known_algs + (..)); + requires \separated(alg, (_alg_id const **)known_algs + (..)); + requires \separated(eaten, (_alg_id const **)known_algs + (..)); + requires \separated(param, (_alg_id const **)known_algs + (..)); + ensures \separated(alg, (_alg_id const **)known_algs + (..)); + */ +static int parse_x509_AlgorithmIdentifier(u8 const *buf, u16 len, + _alg_id const **alg, + alg_param *param, u16 *eaten); +src/x509-parser.c:3487:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_dn_by_oid'returning pointer type. +Callers assumptions might be imprecise. +src/x509-parser.c:4386:[wp] warning: Memory model hypotheses for function 'parse_x509_subjectPublicKeyInfo': +/*@ + behavior wp_typed: + requires \separated(buf + (..), (_alg_id const **)known_algs + (..)); + requires \separated(eaten, (_alg_id const **)known_algs + (..)); + */ +static int parse_x509_subjectPublicKeyInfo(u8 const *buf, u16 len, u16 *eaten); +src/x509-parser.c:7194:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_kp_by_oid'returning pointer type. +Callers assumptions might be imprecise. +src/x509-parser.c:8065:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_ext_by_oid'returning pointer type. +Callers assumptions might be imprecise. +src/x509-parser.c:8108:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*(parsed_oid_list + + (0 .. + sizeof(known_ext_oids) / + sizeof(known_ext_oids[0]) + - 1))'. +Callers assumptions might be imprecise. +src/x509-parser.c:8178:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*(parsed_oid_list + + (0 .. + sizeof(known_ext_oids) / + sizeof(known_ext_oids[0]) + - 1))'. +Callers assumptions might be imprecise. +src/x509-parser.c:8489:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*sig_alg'. +Callers assumptions might be imprecise. +src/x509-parser.c:8491:[wp] warning: Memory model hypotheses for function 'parse_x509_tbsCertificate': +/*@ + behavior wp_typed: + requires \separated(buf + (..), (_alg_id const **)known_algs + (..)); + requires \separated(eaten, (_alg_id const **)known_algs + (..)); + requires \separated(sig_alg, (_alg_id const **)known_algs + (..)); + ensures \separated(sig_alg, (_alg_id const **)known_algs + (..)); + */ +static int parse_x509_tbsCertificate(u8 const *buf, u16 len, + _alg_id const **sig_alg, u16 *eaten); +src/x509-parser.c:8821:[wp] warning: Memory model hypotheses for function 'parse_x509_signatureAlgorithm': +/*@ + behavior wp_typed: + requires \separated(buf + (..), (_alg_id const **)known_algs + (..)); + requires + \separated(exp_sig_alg + (..), (_alg_id const **)known_algs + (..)); + requires \separated(eaten, (_alg_id const **)known_algs + (..)); + */ +static int parse_x509_signatureAlgorithm(u8 const *buf, u16 len, + _alg_id const *exp_sig_alg, + u16 *eaten);