[debie1] further improve analysis; only 2 remaining alarms

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

 directory	file	line	function	property kind	status	property
-code	tc_hand.c	1037	UpdateTarget	initialization	Unknown	\initialized(&SU_setting.execution_result)
 code	telem.c	133	TM_InterruptService	ptr_comparison	Unknown	\pointer_comparable((void *)telemetry_pointer, (void *)(&telemetry_data.time))
 code/harness	harness.c	1020	Start_Conversion	index_bound	Unknown	channel < 0x28
-code/harness	harness.c	3338	Acquisition_Tests	signed_overflow	Unknown	octets + 2 ≤ 2147483647

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

@@ -14,7 +14,7 @@ Initializer of hit_task references HitTriggerTask (at code/measure.c:544)
 Initializer of TC_task references TelecommandExecutionTask (at code/tc_hand.c:1596)
 [metrics] Statements analyzed by Eva
 --------------------------
-2974 stmts in analyzed functions, 2930 stmts analyzed (98.5%)
+2974 stmts in analyzed functions, 2913 stmts analyzed (97.9%)
 Acquire_Hit: 4 stmts out of 4 (100.0%)
 Acquisition_Tests: 132 stmts out of 132 (100.0%)
 AttachInterrupt: 1 stmts out of 1 (100.0%)
@@ -49,7 +49,6 @@ Event_Flag: 1 stmts out of 1 (100.0%)
 ExceedsLimit: 7 stmts out of 7 (100.0%)
 Exec_TC: 3 stmts out of 3 (100.0%)
 ExecuteChannelTest: 61 stmts out of 61 (100.0%)
-ExecuteCommand: 81 stmts out of 81 (100.0%)
 Fail_Check: 2 stmts out of 2 (100.0%)
 FindMinQualityRecord: 19 stmts out of 19 (100.0%)
 FlushMail: 2 stmts out of 2 (100.0%)
@@ -87,7 +86,6 @@ Init_SU_Settings: 14 stmts out of 14 (100.0%)
 LowVoltageCurrent: 12 stmts out of 12 (100.0%)
 MeasureTemperature: 22 stmts out of 22 (100.0%)
 MeasureVoltage: 27 stmts out of 27 (100.0%)
-MemoryPatch: 42 stmts out of 42 (100.0%)
 Monitor: 49 stmts out of 49 (100.0%)
 Monitor_DPU_Voltage: 13 stmts out of 13 (100.0%)
 Monitor_Health: 6 stmts out of 6 (100.0%)
@@ -165,7 +163,6 @@ Trigger_SU_Hit: 3 stmts out of 3 (100.0%)
 Trigger_Source_0: 1 stmts out of 1 (100.0%)
 Trigger_Source_1: 1 stmts out of 1 (100.0%)
 UpdatePeriodCounter: 4 stmts out of 4 (100.0%)
-UpdateTarget: 154 stmts out of 154 (100.0%)
 UpdateTime: 2 stmts out of 2 (100.0%)
 Update_ADC_Channel_Reg: 1 stmts out of 1 (100.0%)
 Update_SU_State: 8 stmts out of 8 (100.0%)
@@ -174,24 +171,27 @@ WaitInterrupt: 1 stmts out of 1 (100.0%)
 WaitInterval: 1 stmts out of 1 (100.0%)
 WaitMail: 9 stmts out of 9 (100.0%)
 WaitTimeout: 1 stmts out of 1 (100.0%)
-WriteMemory: 18 stmts out of 18 (100.0%)
 Write_TM_LSB: 2 stmts out of 2 (100.0%)
 Write_TM_MSB: 2 stmts out of 2 (100.0%)
 isr_send_message: 3 stmts out of 3 (100.0%)
+UpdateTarget: 153 stmts out of 154 (99.4%)
 ClassifyEvent: 59 stmts out of 60 (98.3%)
 TM_Tests: 51 stmts out of 52 (98.1%)
+MemoryPatch: 41 stmts out of 42 (97.6%)
 HandleAcquisition: 57 stmts out of 59 (96.6%)
 StartSystem: 19 stmts out of 20 (95.0%)
 TC_InterruptService: 117 stmts out of 126 (92.9%)
 TM_InterruptService: 25 stmts out of 27 (92.6%)
 SetTriggerLevel: 29 stmts out of 32 (90.6%)
+ExecuteCommand: 73 stmts out of 81 (90.1%)
 Switch_SU_Off: 16 stmts out of 18 (88.9%)
 Switch_SU_On: 16 stmts out of 18 (88.9%)
+WriteMemory: 16 stmts out of 18 (88.9%)
 Start_SU_SwitchingOn: 7 stmts out of 8 (87.5%)
 Check_Current: 13 stmts out of 15 (86.7%)
 PatchExecCommandOk: 5 stmts out of 6 (83.3%)
 CreateTask: 8 stmts out of 10 (80.0%)
 SendTaskMail: 4 stmts out of 5 (80.0%)
 Check_RAM: 22 stmts out of 28 (78.6%)
-Monitor_SU_Voltage: 16 stmts out of 22 (72.7%)
 main: 5 stmts out of 7 (71.4%)
+Monitor_SU_Voltage: 11 stmts out of 22 (50.0%)

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

@@ -5239,6 +5239,7 @@ static void Acquisition_Tests(void)
   hit_budget_left = (unsigned int)(10 + 2);
   Check_Zero((int)event_queue_length);
   octets = 0;
+  /*@ loop unroll 17676; */
   while (mail_count[0] == 0) {
     if (telemetry_pointer < telemetry_end_pointer) TM_InterruptService();
     else TM_InterruptService();

debie1/code/harness/harness.c

@@ -3319,7 +3319,7 @@ static void Acquisition_Tests (void)
       Check_Zero (event_queue_length);
 
       octets = 0;
-      /* @ loop unroll 17676; */
+      /*@ loop unroll 17676; */
       while (mail_count[TCTM_MAILBOX] == 0)
       {
          if (telemetry_pointer < telemetry_end_pointer)