Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
open-source-case-studies
Commits
10d81544
Commit
10d81544
authored
Jun 24, 2021
by
David Bühler
Browse files
[debie1] Adds more loop unrolling, removes slevel; only 1 remaining alarm.
parent
92d547c0
Pipeline
#36090
passed with stage
in 86 minutes and 34 seconds
Changes
6
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
debie1/.frama-c/GNUmakefile
View file @
10d81544
...
...
@@ -25,8 +25,7 @@ FCFLAGS += \
EVAFLAGS
+=
\
-eva-warn-key
builtins:missing-spec
=
abort
\
-eva-domains
equality
\
-eva-auto-loop-unroll
128
\
-eva-slevel
11
\
-eva-auto-loop-unroll
180
\
# -eva-slevel 10 seems insufficient to remove the 5th alarm
# -eva-auto-loop-unroll is also necessary to avoid a 5th alarm
...
...
debie1/.frama-c/debie1.eva/alarms.csv
View file @
10d81544
directory file line function property kind status property
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
debie1/.frama-c/debie1.eva/metrics.log
View file @
10d81544
...
...
@@ -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, 291
3
stmts analyzed (97.9%)
2974 stmts in analyzed functions, 291
1
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%)
...
...
@@ -128,7 +128,6 @@ SetInterruptMask: 2 stmts out of 2 (100.0%)
SetMemoryConfiguration: 7 stmts out of 7 (100.0%)
SetMode: 2 stmts out of 2 (100.0%)
SetModeStatusError: 2 stmts out of 2 (100.0%)
SetSensorUnitOff: 9 stmts out of 9 (100.0%)
SetSoftwareError: 2 stmts out of 2 (100.0%)
SetTestPulseLevel: 2 stmts out of 2 (100.0%)
SetTimeSlice: 1 stmts out of 1 (100.0%)
...
...
@@ -149,7 +148,6 @@ SignalMemoryErrors: 11 stmts out of 11 (100.0%)
SignalPeakDetectorReset: 1 stmts out of 1 (100.0%)
Sim_Self_Test_Trigger: 7 stmts out of 7 (100.0%)
Start_Conversion: 24 stmts out of 24 (100.0%)
Switch_SU_State: 14 stmts out of 14 (100.0%)
TC_ISR_Tests: 51 stmts out of 51 (100.0%)
TC_Interrupt: 2 stmts out of 2 (100.0%)
TC_Task_Tests: 263 stmts out of 263 (100.0%)
...
...
@@ -180,10 +178,12 @@ 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%)
Switch_SU_State: 13 stmts out of 14 (92.9%)
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%)
SetSensorUnitOff: 8 stmts out of 9 (88.9%)
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%)
...
...
debie1/.frama-c/debie1.eva/nonterm.log
View file @
10d81544
code/debie.c:50:[nonterm:unreachable] warning: unreachable implicit return
code/harness/harness.c:373
2
:[nonterm:unreachable] warning: unreachable implicit return
code/harness/harness.c:373
4
:[nonterm:unreachable] warning: unreachable implicit return
debie1/.frama-c/debie1.parse/framac.ast
View file @
10d81544
...
...
@@ -5330,6 +5330,7 @@ void SU_Self_Test_Tests(void)
Check_Zero((int)telemetry_data.error_status & 1);
Check_Nonzero(self_test_SU_number == (sensor_number_t)2);
Check_No_Errors();
/*@ loop unroll 10; */
while (health_mon_round != (uint_least8_t)round_7_e) Monitor_Health(61);
Check_Nonzero(self_test_SU_number == (sensor_number_t)2);
Check_Nonzero(SU_state[1] == (unsigned int)self_test_mon_e);
...
...
@@ -5349,6 +5350,7 @@ void SU_Self_Test_Tests(void)
Check_Nonzero(self_test_SU_number == (sensor_number_t)2);
Check_Nonzero(SU_state[1] == (unsigned int)self_test_mon_e);
sim_self_test = (unsigned char)0;
/*@ loop unroll 10; */
while (health_mon_round != (uint_least8_t)round_7_e) Monitor_Health(61);
Check_Nonzero(self_test_SU_number == (sensor_number_t)2);
Check_Nonzero(SU_state[1] == (unsigned int)self_test_mon_e);
...
...
debie1/code/harness/harness.c
View file @
10d81544
...
...
@@ -3487,6 +3487,7 @@ void SU_Self_Test_Tests (void)
/* Run Monitoring up to but not including round_7_e: */
//@ loop unroll 10;
while
(
health_mon_round
!=
round_7_e
)
{
Monitor_Health
(
Prob6a
);
...
...
@@ -3530,6 +3531,7 @@ void SU_Self_Test_Tests (void)
/* Run Monitoring up to but not including round_7_e: */
//@ loop unroll 10;
while
(
health_mon_round
!=
round_7_e
)
{
Monitor_Health
(
Prob6a
);
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment