diff --git a/debie1/.frama-c/debie1.eva/metrics.log b/debie1/.frama-c/debie1.eva/metrics.log index 517108efefef87fde8ccc48c69a91f82dac0f892..7efca3eb62e89f1b10ec6286f64bb0fb5f1a5f57 100644 --- a/debie1/.frama-c/debie1.eva/metrics.log +++ b/debie1/.frama-c/debie1.eva/metrics.log @@ -9,12 +9,12 @@ Unreached functions (3) = <code/tc_hand.c>: TelecommandExecutionTask; [metrics] References to non-analyzed functions ------------------------------------ -Initializer of acq_task references AcquisitionTask (at code/measure.c:545) -Initializer of hit_task references HitTriggerTask (at code/measure.c:544) +Initializer of acq_task references AcquisitionTask (at code/measure.c:544) +Initializer of hit_task references HitTriggerTask (at code/measure.c:543) Initializer of TC_task references TelecommandExecutionTask (at code/tc_hand.c:1596) [metrics] Statements analyzed by Eva -------------------------- -3243 stmts in analyzed functions, 3172 stmts analyzed (97.8%) +3242 stmts in analyzed functions, 3171 stmts analyzed (97.8%) Acquire_Hit: 10 stmts out of 10 (100.0%) Acquisition_Tests: 157 stmts out of 157 (100.0%) AttachInterrupt: 2 stmts out of 2 (100.0%) @@ -175,7 +175,7 @@ isr_send_message: 4 stmts out of 4 (100.0%) UpdateTarget: 153 stmts out of 154 (99.4%) ClassifyEvent: 59 stmts out of 60 (98.3%) MemoryPatch: 41 stmts out of 42 (97.6%) -HandleAcquisition: 59 stmts out of 61 (96.7%) +HandleAcquisition: 58 stmts out of 60 (96.7%) StartSystem: 23 stmts out of 24 (95.8%) Switch_SU_State: 13 stmts out of 14 (92.9%) TC_InterruptService: 117 stmts out of 126 (92.9%) diff --git a/debie1/.frama-c/debie1.parse/framac.ast b/debie1/.frama-c/debie1.parse/framac.ast index 1e15d5e9c3f979e8513440b780d0721cdd2a9389..93b93d8613d33bfb836498adc52418a8aaaaed59 100644 --- a/debie1/.frama-c/debie1.parse/framac.ast +++ b/debie1/.frama-c/debie1.parse/framac.ast @@ -2412,7 +2412,6 @@ void HandleAcquisition(void) unsigned char tmp; _LOR: tmp = Event_Flag(); if ((int)tmp == 1) { - /*@ \eva::split event_queue_length; */ ; event = GetFreeRecord(); event->SU_number = (unsigned char)((int)trigger_unit & 0xFF); memcpy((void *)(& event->plasma_1_plus), diff --git a/debie1/.frama-c/debie1.parse/metrics.log b/debie1/.frama-c/debie1.parse/metrics.log index 04181ff927ab10d6606d81b8d7b228228b8973fa..5bebf5ec6523323d05934345af0a2552916baf44 100644 --- a/debie1/.frama-c/debie1.parse/metrics.log +++ b/debie1/.frama-c/debie1.parse/metrics.log @@ -100,7 +100,7 @@ Potential entry points (8) Global metrics ============== -Sloc = 3347 +Sloc = 3346 Decision point = 418 Global variables = 104 If = 311 diff --git a/debie1/code/measure.c b/debie1/code/measure.c index ce6c29415984478e6b9b0c1ec92521244b67fb82..ad126bafd16457fe5b19e19397975b0fac429602 100644 --- a/debie1/code/measure.c +++ b/debie1/code/measure.c @@ -405,7 +405,6 @@ void HandleAcquisition (void) if ((state == self_test_e || state == acquisition_e) && (EVENT_FLAG == ACCEPT_EVENT)) { - /*@ split event_queue_length; */ event = GetFreeRecord(); /* Get pointer to the new event record. */