[papabench] remove volatile modifier to avoid overly imprecise results;...

[papabench] remove volatile modifier to avoid overly imprecise results; improve analysis parametrization

papabench/.frama-c/GNUmakefile

@@ -32,7 +32,7 @@ FCFLAGS     += \
 ## Eva-specific flags
 EVAFLAGS    += \
   -eva-warn-key builtins:missing-spec=abort \
-  -eva-slevel 1 \
+  -eva-precision 1 \
 
 ## GUI-only flags
 FCGUIFLAGS += \

papabench/.frama-c/papabench.eva/alarms.csv

@@ -26,16 +26,8 @@ sw/airborne/autopilot	main.c	582	stabilisation_task	float_to_int	Unknown	tmp < 3
 sw/airborne/autopilot	main.c	582	stabilisation_task	is_nan_or_infinite	Unknown	\is_finite(tmp)
 sw/airborne/autopilot	main.c	608	send_gps_pos	index_bound	Unknown	tx_tail < 255
 sw/airborne/autopilot	main.c	615	send_radIR	index_bound	Unknown	tx_tail < 255
-sw/airborne/autopilot	main.c	620	send_takeOff	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
 sw/airborne/autopilot	main.c	623	send_takeOff	index_bound	Unknown	tx_tail < 255
-sw/airborne/autopilot	nav.c	130	approaching	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
 sw/airborne/autopilot	nav.c	159	route_to	is_nan	Unknown	¬\is_NaN(\div_float(\add_float(\mul_float(\sub_float(estimator_x, last_wp_x), leg_x), \mul_float(\sub_float(estimator_y, last_wp_y), leg_y)), leg2))
-sw/airborne/autopilot	nav.c	162	route_to	is_nan	Unknown	¬\is_NaN(\add_double((double)alpha, tmp_0))
-sw/airborne/autopilot	nav.c	162	route_to	is_nan	Unknown	¬\is_NaN(\div_float(carrot, leg))
-sw/airborne/autopilot	nav.c	164	route_to	is_nan	Unknown	¬\is_NaN(\mul_float(alpha, leg_x))
-sw/airborne/autopilot	nav.c	164	route_to	is_nan	Unknown	¬\is_NaN(\mul_float(alpha, leg_y))
-sw/airborne/autopilot	nav.c	181	nav_home	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/airborne/autopilot	nav.c	181	nav_home	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
 sw/airborne/autopilot	pid.c	54	roll_pitch_pid_run	float_to_int	Unknown	-32769 < tmp
 sw/airborne/autopilot	pid.c	54	roll_pitch_pid_run	float_to_int	Unknown	tmp < 32768
 sw/airborne/autopilot	pid.c	54	roll_pitch_pid_run	is_nan_or_infinite	Unknown	\is_finite(tmp)
@@ -45,16 +37,5 @@ sw/airborne/autopilot	pid.c	58	roll_pitch_pid_run	float_to_int	Unknown	tmp_1 < 3
 sw/airborne/autopilot	pid.c	58	roll_pitch_pid_run	is_nan_or_infinite	Unknown	\is_finite(tmp_1)
 sw/airborne/autopilot	pid.c	114	climb_pid_run	float_to_int	Unknown	-32769 < tmp
 sw/airborne/autopilot	pid.c	114	climb_pid_run	float_to_int	Unknown	tmp < 32768
-sw/lib/c	pp_math.c	34	pp_atan2	is_nan	Unknown	¬\is_NaN(\div_double(\sub_double(x, abs_y), \add_double(x, abs_y)))
-sw/lib/c	pp_math.c	34	pp_atan2	is_nan	Unknown	¬\is_NaN(\sub_double(x, abs_y))
-sw/lib/c	pp_math.c	39	pp_atan2	is_nan	Unknown	¬\is_NaN(\div_double(\add_double(x, abs_y), \sub_double(abs_y, x)))
 sw/lib/c	pp_math.c	87	pp_sqrt	is_nan	Unknown	¬\is_NaN(\add_double((double)x, \div_double(n, (double)x)))
 sw/lib/c	pp_math.c	87	pp_sqrt	is_nan	Unknown	¬\is_NaN(\div_double(n, (double)x))
-sw/var/include	flight_plan.h	423	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/var/include	flight_plan.h	423	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/var/include	flight_plan.h	445	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/var/include	flight_plan.h	445	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/var/include	flight_plan.h	472	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/var/include	flight_plan.h	472	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/var/include	flight_plan.h	484	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)
-sw/var/include	flight_plan.h	484	auto_nav	is_nan	Unknown	¬\is_NaN(estimator_hspeed_mod)

papabench/.frama-c/papabench.eva/metrics.log

@@ -7,7 +7,7 @@ Coverage estimation = 100.0%
 ------------------------------------
 [metrics] Statements analyzed by Eva
 --------------------------
-3720 stmts in analyzed functions, 3673 stmts analyzed (98.7%)
+3720 stmts in analyzed functions, 3668 stmts analyzed (98.6%)
 adc_buf_channel: 2 stmts out of 2 (100.0%)
 adc_init: 12 stmts out of 12 (100.0%)
 altitude_control_task: 7 stmts out of 7 (100.0%)
@@ -69,8 +69,8 @@ timer_periodic_0: 7 stmts out of 7 (100.0%)
 uart1_init: 7 stmts out of 7 (100.0%)
 periodic_task: 51 stmts out of 52 (98.1%)
 roll_pitch_pid_run: 25 stmts out of 26 (96.2%)
-auto_nav: 665 stmts out of 694 (95.8%)
-nav_home: 38 stmts out of 40 (95.0%)
+auto_nav: 661 stmts out of 694 (95.2%)
 main: 30 stmts out of 32 (93.8%)
+nav_home: 37 stmts out of 40 (92.5%)
 estimator_update_state_infrared: 8 stmts out of 9 (88.9%)
 climb_pid_run: 21 stmts out of 32 (65.6%)

papabench/.frama-c/papabench.parse/framac.ast

@@ -230,7 +230,7 @@ float estimator_phi_dot;
 float estimator_psi_dot;
 uint16_t estimator_flight_time;
 float estimator_t;
-float volatile estimator_hspeed_mod;
+float estimator_hspeed_mod;
 float estimator_hspeed_dir;
 void estimator_init(void);
 

papabench/sw/airborne/autopilot/estimator.c

@@ -58,7 +58,7 @@ uint16_t estimator_flight_time;
 float estimator_t; 
 
 /* horizontal speed in module and dir */
-volatile float estimator_hspeed_mod;
+float estimator_hspeed_mod;
 float estimator_hspeed_dir;
 
 float estimator_rad_of_ir, estimator_ir, estimator_rad;

papabench/sw/airborne/autopilot/estimator.h

@@ -52,7 +52,7 @@ extern uint16_t estimator_flight_time;
 extern float estimator_t;
 
 /* horizontal speed in module and dir (m/s, rad) */
-extern volatile float estimator_hspeed_mod;
+extern float estimator_hspeed_mod;
 extern float estimator_hspeed_dir;
 
 void estimator_init( void );