Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
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
7ed51c66
Commit
7ed51c66
authored
Jun 07, 2021
by
Andre Maroneze
💬
Browse files
Merge branch 'fix-papabench' into 'master'
sync with frama-c master; fix papabench's math.h inclusion See merge request
!19
parents
e3817b1c
51335553
Pipeline
#35650
passed with stage
in 69 minutes and 19 seconds
Changes
24
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
.gitlab-ci.yml
View file @
7ed51c66
default
:
image
:
framac/frama-c:dev
image
:
framac/frama-c:dev
-stripped
build
:
tags
:
...
...
chrony/.frama-c/chrony-ntp-core.eva/alarms.csv
View file @
7ed51c66
...
...
@@ -854,10 +854,10 @@ FRAMAC_SHARE/libc string.h 118 memset precondition Unknown valid_s: valid_or_emp
FRAMAC_SHARE/libc string.h 128 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 160 strchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc unistd.h 774 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 11
16
unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 11
23
unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from \nothing;
FRAMAC_SHARE/libc/sys stat.h 8
4
stat precondition Unknown valid_pathname: valid_read_string(pathname)
FRAMAC_SHARE/libc/sys stat.h 8
7
stat precondition Unknown valid_pathname: valid_read_string(pathname)
test/unit ntp_core.c 179 send_response precondition of __FC_assert Invalid or unreachable nonnull_c: c ≢ 0
test/unit ntp_core.c 186 send_response precondition of __FC_assert Unknown nonnull_c: c ≢ 0
test/unit ntp_core.c 192 send_response precondition of __FC_assert Invalid or unreachable nonnull_c: c ≢ 0
...
...
frama-c
@
e9b10643
Compare
87773f21
...
e9b10643
Subproject commit
87773f21079cd7b964a153405f088937a896ca53
Subproject commit
e9b106433ad0ae49c91648dfefbd051624525375
gzip124/.frama-c/gzip124.eva/alarms.csv
View file @
7ed51c66
...
...
@@ -647,7 +647,7 @@ directory file line function property kind status property
. zip.c 111 file_read precondition of read Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
. zip.c 111 file_read precondition of read Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc ctype.h 174 isupper precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc fcntl.h 1
57
__va_open_mode_t precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc fcntl.h 1
61
__va_open_mode_t precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.h 266 fgets precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 323 putc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 447 fileno precondition Unknown valid_stream: \valid(stream)
...
...
@@ -677,15 +677,15 @@ FRAMAC_SHARE/libc string.h 412 strcat precondition Unknown valid_string_dest: va
FRAMAC_SHARE/libc string.h 413 strcat precondition Unknown room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
FRAMAC_SHARE/libc unistd.h 774 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 782 close precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 96
5
lseek precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
4
read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
5
read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 11
16
unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 113
2
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
33
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 96
7
lseek precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
6
read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
7
read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 11
23
unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 113
9
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
40
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from \nothing;
FRAMAC_SHARE/libc/sys stat.h 3
4
fstat assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 3
4
fstat from clause Unknown assigns \result \from \nothing;
FRAMAC_SHARE/libc/sys stat.h 4
0
lstat precondition Unknown valid_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 8
4
stat precondition Unknown valid_pathname: valid_read_string(pathname)
FRAMAC_SHARE/libc/sys stat.h 3
5
fstat assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 3
5
fstat from clause Unknown assigns \result \from \nothing;
FRAMAC_SHARE/libc/sys stat.h 4
3
lstat precondition Unknown valid_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 8
7
stat precondition Unknown valid_pathname: valid_read_string(pathname)
hiredis/.frama-c/hiredis-misc.eva/alarms.csv
View file @
7ed51c66
...
...
@@ -309,7 +309,7 @@ directory file line function property kind status property
. test.c 1015 main precondition of access Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Invalid or unreachable nonnull_c: c ≢ 0
FRAMAC_SHARE/libc ctype.h 134 isprint precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc netdb.h 1
17
freeaddrinfo precondition Unknown addrinfo_valid: \valid(addrinfo)
FRAMAC_SHARE/libc netdb.h 1
25
freeaddrinfo precondition Unknown addrinfo_valid: \valid(addrinfo)
FRAMAC_SHARE/libc stdlib.h 78 atoi precondition Unknown valid_nptr: \valid_read(nptr)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc stdlib.h 422 realloc precondition Unknown freeable: ptr ≡ \null ∨ \freeable(ptr)
...
...
kilo/.frama-c/kilo.eva/alarms.csv
View file @
7ed51c66
...
...
@@ -560,7 +560,7 @@ directory file line function property kind status property
FRAMAC_SHARE/libc ctype.h 94 isdigit precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc ctype.h 134 isprint precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc ctype.h 161 isspace precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc fcntl.h 1
57
__va_open_mode_t precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc fcntl.h 1
61
__va_open_mode_t precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.c 68 getline mem_access Unknown \valid(*lineptr + tmp_2)
FRAMAC_SHARE/libc stdio.c 71 getline mem_access Unknown \valid(*lineptr + cur)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
...
...
@@ -583,7 +583,7 @@ FRAMAC_SHARE/libc string.h 108 memmove precondition Unknown valid_src: valid_rea
FRAMAC_SHARE/libc string.h 118 memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc string.h 128 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc unistd.h 782 close precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 86
4
ftruncate assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc unistd.h 86
4
ftruncate from clause Unknown assigns \result \from \nothing;
FRAMAC_SHARE/libc unistd.h 113
2
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
33
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 86
6
ftruncate assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc unistd.h 86
6
ftruncate from clause Unknown assigns \result \from \nothing;
FRAMAC_SHARE/libc unistd.h 113
9
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
40
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
libmodbus/.frama-c/libmodbus-unit-server.eva/alarms.csv
View file @
7ed51c66
...
...
@@ -6,10 +6,10 @@ FRAMAC_SHARE/libc string.h 95 memcpy precondition Unknown valid_dest: valid_or_e
FRAMAC_SHARE/libc string.h 96 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc time.h 288 nanosleep precondition Unknown valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000
FRAMAC_SHARE/libc unistd.h 782 close precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
4
read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
5
read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 113
2
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
33
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 100
6
read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
7
read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 113
9
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
40
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc/sys socket.h 301 accept precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 436 recv precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 437 recv precondition Unknown valid_buffer_length: \valid((char *)buf + (0 .. len - 1))
...
...
microstrain/.frama-c/microstrain_gx4_45_test.eva/alarms.csv
View file @
7ed51c66
directory file line function property kind status property
FRAMAC_SHARE/libc fcntl.h 15
0
__va_open_void precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc fcntl.h 15
4
__va_open_void precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdlib.h 564 abs precondition Unknown abs_representable: j > -2147483647 - 1
FRAMAC_SHARE/libc string.h 95 memcpy precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 96 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 355 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 413 strcat precondition Unknown room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
FRAMAC_SHARE/libc unistd.h 100
4
read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
5
read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 113
2
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
33
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 100
6
read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 100
7
read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 113
9
write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 11
40
write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test GX4-45_Test.c 258 main precondition of printf_va_25 Unknown valid_read_string(param0)
MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test GX4-45_Test.c 258 printf_va_25 precondition Unknown valid_read_string(param0)
MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test GX4-45_Test.c 261 main precondition of printf_va_26 Unknown valid_read_string(param0)
...
...
papabench/.frama-c/GNUmakefile
View file @
7ed51c66
...
...
@@ -20,7 +20,7 @@ CPPFLAGS += \
-I
../sw/var/include
\
-I
../sw/airborne/autopilot
\
-I
../avr/include
\
-
iquote
../sw/include
\
-
I
../sw/include
\
## General flags
FCFLAGS
+=
\
...
...
@@ -43,9 +43,8 @@ TARGETS = papabench.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
papabench.parse
:
\
$(sort $(wildcard ../sw/airborne/autopilot/*.c))
\
../sw/lib/c/math.c
\
../sw/lib/c/
pp_
math.c
\
$(shell $(FRAMAC)-config -print-share-path)/libc/math.c
\
fc_stubs.h
\
### Epilogue. Do not modify this block. #######################################
...
...
papabench/.frama-c/fc_stubs.h
deleted
100644 → 0
View file @
e3817b1c
/*@
requires valid_exp: \valid(exp);
assigns \result, *exp \from x;
*/
float
frexpf
(
float
x
,
int
*
exp
);
/*@
assigns \result \from x, exp;
*/
double
ldexp
(
double
x
,
int
exp
);
papabench/.frama-c/papabench.eva/alarms.csv
View file @
7ed51c66
...
...
@@ -41,21 +41,18 @@ sw/airborne/autopilot nav.c 181 nav_home precondition of pp_sin Unknown \is_fini
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)
sw/airborne/autopilot pid.c 57 roll_pitch_pid_run is_nan Unknown ¬\is_NaN(\mul_
double((double)
pitch_of_roll, tmp_0))
sw/airborne/autopilot pid.c 57 roll_pitch_pid_run is_nan Unknown ¬\is_NaN(\mul_
float(
pitch_of_roll, tmp_0))
sw/airborne/autopilot pid.c 58 roll_pitch_pid_run float_to_int Unknown -32769 < tmp_1
sw/airborne/autopilot pid.c 58 roll_pitch_pid_run float_to_int Unknown tmp_1 < 32768
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 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 math.c 34 pp_atan2 is_nan Unknown ¬\is_NaN(\sub_double(x, abs_y))
sw/lib/c 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 math.c 54 pp_sin precondition Unknown \is_finite(x)
sw/lib/c math.c 86 pp_sqrt initialization Unknown \initialized(&e)
sw/lib/c math.c 86 pp_sqrt is_nan Unknown ¬\is_NaN(m)
sw/lib/c math.c 86 pp_sqrt is_nan Unknown ¬\is_NaN(tmp)
sw/lib/c math.c 91 pp_sqrt is_nan Unknown ¬\is_NaN(\add_double((double)x, \div_double(n, (double)x)))
sw/lib/c math.c 91 pp_sqrt is_nan Unknown ¬\is_NaN(\div_double(n, (double)x))
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 54 pp_sin precondition Unknown \is_finite(x)
sw/lib/c pp_math.c 91 pp_sqrt is_nan Unknown ¬\is_NaN(\add_double((double)x, \div_double(n, (double)x)))
sw/lib/c pp_math.c 91 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 423 auto_nav is_nan Unknown ¬\is_NaN(estimator_hspeed_mod)
...
...
papabench/.frama-c/papabench.eva/metrics.log
View file @
7ed51c66
...
...
@@ -7,7 +7,7 @@ Coverage estimation = 100.0%
------------------------------------
[metrics] Statements analyzed by Eva
--------------------------
37
15
stmts in analyzed functions, 36
68
stmts analyzed (98.7%)
37
20
stmts in analyzed functions, 36
73
stmts analyzed (98.7%)
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%)
...
...
@@ -42,7 +42,7 @@ nav_update: 3 stmts out of 3 (100.0%)
navigation_update: 5 stmts out of 5 (100.0%)
parse_gps_msg: 18 stmts out of 18 (100.0%)
parse_ubx: 48 stmts out of 48 (100.0%)
pp_atan2: 1
7
stmts out of 1
7
(100.0%)
pp_atan2: 1
9
stmts out of 1
9
(100.0%)
pp_sin: 20 stmts out of 20 (100.0%)
pp_sqrt: 12 stmts out of 12 (100.0%)
pprz_mode_update__fc_inline: 31 stmts out of 31 (100.0%)
...
...
@@ -68,8 +68,8 @@ timer_init_0: 4 stmts out of 4 (100.0%)
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%)
roll_pitch_pid_run: 22 stmts out of 23 (95.7%)
nav_home: 38 stmts out of 40 (95.0%)
main: 30 stmts out of 32 (93.8%)
estimator_update_state_infrared: 8 stmts out of 9 (88.9%)
...
...
papabench/.frama-c/papabench.parse/framac.ast
View file @
7ed51c66
...
...
@@ -222,6 +222,12 @@ void __vector_21(void)
return;
}
double pp_sin(double x);
double pp_sqrt(double n);
double pp_atan2(double x, double y);
float estimator_x;
float estimator_y;
float estimator_z;
...
...
@@ -428,7 +434,6 @@ void estimator_update_ir_estim(void)
if (estimator_update_ir_estim_initialized) {
float dt = gps_ftow - estimator_update_ir_estim_last_t;
if ((double)dt > 0.1) {
double tmp;
float phi =
estimator_hspeed_dir - estimator_update_ir_estim_last_hspeed_dir;
while ((double)phi > 0x1.921fb54442d18p1) phi = (float)((double)phi -
...
...
@@ -442,8 +447,7 @@ void estimator_update_ir_estim(void)
(double)2 * 0x1.921fb54442d18p1);
estimator_ir = (float)ir_roll;
estimator_rad = phi;
tmp = fabs((double)phi);
absphi = (float)tmp;
if ((double)phi < 0.) absphi = - phi; else absphi = phi;
if ((double)absphi < 1.0)
if ((double)absphi > 0.05)
if (- ((int)ir_contrast) / 2 < (int)ir_roll)
...
...
@@ -3210,12 +3214,6 @@ void __vector_5(void)
return;
}
double pp_sin(double x);
double pp_sqrt(double n);
double pp_atan2(double x, double y);
uint8_t nav_stage;
uint8_t nav_block;
float dist2_to_wp;
...
...
@@ -3273,7 +3271,7 @@ __inline static void auto_nav(void)
goto return_label;
}
else {
desired_course = (float)((270.0 / 180.) *
3.141592653589793238462643
);
desired_course = (float)((270.0 / 180.) *
0x1.921fb54442d18p1
);
auto_pitch = (unsigned char)0;
nav_pitch = (float)0.150000;
vertical_mode = (unsigned char)1;
...
...
@@ -3300,7 +3298,7 @@ __inline static void auto_nav(void)
goto return_label;
}
else {
desired_course = (float)((270.0 / 180.) *
3.141592653589793238462643
);
desired_course = (float)((270.0 / 180.) *
0x1.921fb54442d18p1
);
auto_pitch = (unsigned char)0;
nav_pitch = (float)0.000000;
vertical_mode = (unsigned char)2;
...
...
@@ -3711,7 +3709,7 @@ __inline static void auto_nav(void)
;
fly_to_xy((float)((double)auto_nav_carrot_x + tmp_16 * (double)tmp_17),
(float)((double)auto_nav_carrot_y + tmp_14 * (double)tmp_15));
qdr = (float)(((
3.141592653589793238462643
/ (double)2 - (double)alpha_carrot) /
3.141592653589793238462643
) * 180.);
qdr = (float)(((
0x1.921fb54442d18p1
/ (double)2 - (double)alpha_carrot) /
0x1.921fb54442d18p1
) * 180.);
while (qdr < (float)0) qdr += (float)360;
while (qdr >= (float)360) qdr -= (float)360;
}
...
...
@@ -3783,7 +3781,7 @@ __inline static void auto_nav(void)
;
fly_to_xy((float)((double)waypoints[0].x + tmp_24 * (double)tmp_25),
(float)((double)waypoints[0].y + tmp_22 * (double)tmp_23));
qdr = (float)(((
3.141592653589793238462643
/ (double)2 - (double)alpha_carrot_0) /
3.141592653589793238462643
) * 180.);
qdr = (float)(((
0x1.921fb54442d18p1
/ (double)2 - (double)alpha_carrot_0) /
0x1.921fb54442d18p1
) * 180.);
while (qdr < (float)0) qdr += (float)360;
while (qdr >= (float)360) qdr -= (float)360;
}
...
...
@@ -3868,7 +3866,7 @@ __inline static void auto_nav(void)
;
fly_to_xy((float)((double)waypoints[1].x + tmp_32 * (double)tmp_33),
(float)((double)waypoints[1].y + tmp_30 * (double)tmp_31));
qdr = (float)(((
3.141592653589793238462643
/ (double)2 - (double)alpha_carrot_1) /
3.141592653589793238462643
) * 180.);
qdr = (float)(((
0x1.921fb54442d18p1
/ (double)2 - (double)alpha_carrot_1) /
0x1.921fb54442d18p1
) * 180.);
while (qdr < (float)0) qdr += (float)360;
while (qdr >= (float)360) qdr -= (float)360;
}
...
...
@@ -3920,7 +3918,7 @@ __inline static void auto_nav(void)
;
fly_to_xy((float)((double)waypoints[4].x + tmp_40 * (double)tmp_41),
(float)((double)waypoints[4].y + tmp_38 * (double)tmp_39));
qdr = (float)(((
3.141592653589793238462643
/ (double)2 - (double)alpha_carrot_2) /
3.141592653589793238462643
) * 180.);
qdr = (float)(((
0x1.921fb54442d18p1
/ (double)2 - (double)alpha_carrot_2) /
0x1.921fb54442d18p1
) * 180.);
while (qdr < (float)0) qdr += (float)360;
while (qdr >= (float)360) qdr -= (float)360;
}
...
...
@@ -3996,7 +3994,7 @@ static void fly_to_xy(float x, float y)
desired_x = x;
desired_y = y;
tmp = pp_atan2((double)(y - estimator_y),(double)(x - estimator_x));
desired_course = (float)(
3.141592653589793238462643
/ 2. - tmp);
desired_course = (float)(
0x1.921fb54442d18p1
/ 2. - tmp);
return;
}
...
...
@@ -4066,7 +4064,7 @@ void nav_home(void)
;
fly_to_xy((float)((double)waypoints[0].x + tmp_4 * (double)tmp_5),
(float)((double)waypoints[0].y + tmp_2 * (double)tmp_3));
qdr = (float)(((
3.141592653589793238462643
/ (double)2 - (double)alpha_carrot) /
3.141592653589793238462643
) * 180.);
qdr = (float)(((
0x1.921fb54442d18p1
/ (double)2 - (double)alpha_carrot) /
0x1.921fb54442d18p1
) * 180.);
while (qdr < (float)0) qdr += (float)360;
while (qdr >= (float)360) qdr -= (float)360;
}
...
...
@@ -4104,7 +4102,7 @@ float pitch_of_vz_pgain = (float)0.05;
float pitch_of_vz = (float)0.;
void roll_pitch_pid_run(void)
{
double
tmp_0;
float
tmp_0;
float err = estimator_phi - desired_roll;
if (roll_pgain * err < (float)(- (600 * 16))) desired_aileron = (short)(- (
600 * 16));
...
...
@@ -4115,8 +4113,9 @@ void roll_pitch_pid_run(void)
desired_aileron = (short)tmp;
}
if ((double)pitch_of_roll < 0.) pitch_of_roll = (float)0.;
tmp_0 = fabs((double)estimator_phi);
err = (float)(- ((double)(estimator_theta - desired_pitch) - (double)pitch_of_roll * tmp_0));
if ((double)estimator_phi < 0.) tmp_0 = - estimator_phi;
else tmp_0 = estimator_phi;
err = - ((estimator_theta - desired_pitch) - pitch_of_roll * tmp_0);
if (pitch_pgain * err < (float)(- (600 * 16))) desired_elevator = (short)(- (
600 * 16));
else {
...
...
@@ -4383,7 +4382,7 @@ double pp_atan2(double x, double y)
double r;
double coeff_1 = 0x1.921fb54442d18p1 / (double)4;
double coeff_2 = (double)3 * coeff_1;
tmp = fabs(y)
;
if (y < 0.) tmp = - y; else tmp = y
;
double abs_y = tmp + 1e-10;
if (x > (double)0) {
r = (x - abs_y) / (x + abs_y);
...
...
papabench/.frama-c/papabench.parse/metrics.log
View file @
7ed51c66
...
...
@@ -65,15 +65,15 @@ Potential entry points (29)
Global metrics
==============
Sloc = 39
19
Decision point = 67
1
Sloc = 39
24
Decision point = 67
4
Global variables = 181
If = 67
1
If = 67
4
Loop = 23
Goto = 87
Assignment = 23
09
Assignment = 23
11
Exit point = 98
Function = 98
Function call = 11
5
Function call = 11
2
Pointer dereferencing = 623
Cyclomatic complexity = 7
69
Cyclomatic complexity = 7
72
papabench/sw/airborne/autopilot/estimator.c
View file @
7ed51c66
...
...
@@ -23,7 +23,7 @@
*/
#include <inttypes.h>
#include <math.h>
#include <
pp_
math.h>
#include "estimator.h"
#include "gps.h"
...
...
papabench/sw/airborne/autopilot/gps_ubx.c
View file @
7ed51c66
...
...
@@ -27,7 +27,7 @@
#include <avr/signal.h>
#include <avr/interrupt.h>
//#include <string.h>
#include <math.h>
#include <
pp_
math.h>
#include "flight_plan.h"
#include "uart.h"
...
...
papabench/sw/airborne/autopilot/main.c
View file @
7ed51c66
...
...
@@ -26,7 +26,7 @@
*
*/
#include <inttypes.h>
#include <math.h>
#include <
pp_
math.h>
#include "link_autopilot.h"
...
...
papabench/sw/airborne/autopilot/nav.c
View file @
7ed51c66
...
...
@@ -24,7 +24,7 @@
#define NAV_C
#include "math.h"
#include "
pp_
math.h"
#include "nav.h"
#include "estimator.h"
...
...
papabench/sw/airborne/autopilot/pid.c
View file @
7ed51c66
...
...
@@ -28,7 +28,7 @@
*/
//#include <stdlib.h>
#include <math.h>
#include <
pp_
math.h>
#include "pid.h"
...
...
papabench/sw/include/c/geometry.h
View file @
7ed51c66
...
...
@@ -28,7 +28,7 @@
#ifndef GEOMETRY_H
#define GEOMETRY_H
#include <math.h>
#include <
pp_
math.h>
#include "angles.h"
/*
please use
...
...
Prev
1
2
Next
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