[x509-parser] Eva original options

x509-parser/.frama-c/GNUmakefile

@@ -32,7 +32,19 @@ FCFLAGS     += \
 EVAFLAGS    += \
   -eva-warn-key builtins:missing-spec=abort \
   -eva-precision 2 \
-  -eva-slevel-function parse_x509_AlgorithmIdentifier:12 \
+  -eva-slevel-function="_extract_complex_tag:100, \
+				      _parse_arc:100, \
+				      parse_UTCTime:100, \
+				      find_dn_by_oid:100, \
+				      find_curve_by_oid:100, \
+				      find_alg_by_oid:200, \
+				      find_ext_by_oid:200, \
+				      parse_AccessDescription:400, \
+				      parse_x509_Extension:400, \
+				      parse_x509_subjectPublicKeyInfo:300, \
+				      parse_x509_Extensions:400, \
+				      parse_x509_tbsCertificate:400, \
+				      parse_x509_AlgorithmIdentifier:200" \
   -eva-warn-undefined-pointer-comparison none \
 
 WPFLAGS += \

x509-parser/.frama-c/x509-parser.wp/alarms.csv

 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