[x509-parser] add optional WP target

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
 ###############################################################################

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

x509-parser/.frama-c/x509-parser.wp/warnings.log

+[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 + (..), &param->curve_param);
+     requires \separated(buf + (..), (_curve const **)known_curves + (..));
+     requires \separated(param, (_curve const **)known_curves + (..));
+     ensures
+       \separated((_curve const **)known_curves + (..), &param->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);