[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Paparazzi-devel] Source code analysis of paparazzi

From: Gautier Hattenberger
Subject: Re: [Paparazzi-devel] Source code analysis of paparazzi
Date: Wed, 05 Nov 2014 11:00:26 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.8.1


It is of course very interesting to have this kind of feedback in order to improve the code.

Concerning the configuration to test, it would be interesting to cover both fixedwing and rotorcraft configuration, and both architecture (lpc2148 and stm32).

Maybe we can help you to choose interesting configuration to test. Which version are you actually using ? (run ./paparazzi_version in a terminal from the main paparazzi folder).

We have met people from your lab at Enac a few years ago, but I don't remember exactly who. Was it your, or your colleagues ?

Gautier Hattenberger

Le 05/11/2014 10:32, Matthieu Lemerre a écrit :

First let me introduce myself: I am a researcher at CEA working on
Frama-C, a source-code analysis platform for C code. I am currently
working with SRI and UCSC on a DARPA project named CHEKOFV, whose goal
is to crowd-source part of verification work by having players finding
verification invariants without knowing, by playing on a game (you can
find the games on To that purpose, we have
chosen Paparazzi to be our next target of verification.

So (if you allow me) I will regularly post on this mailing list to
report to you about potential bugs I found in the source code during the
verification process. Forgive me if I don't use the very latest version
of the code; as I sometimes have to make changes to the source code to
simplify the verification, it is simpler for me if I stick to one
version. Also, I must warn you that I know nothing about UAVs or
Paparazzi configurations.

The first bug I have found happens in the "Booz2" configuration. In
src/sw/airborne/led.h, there is a led_init() function, which calls a
a bunch of LED_INIT macros, one of set translating to:

((gpioRegs_t *)0xE0028000)->dir1 |= (unsigned long)(1 << 31);

This code is incorrect, as 1 is signed, 1 << 31 results in a signed
overflow which is an undefined behaviour. The correct replacement is
((unsigned long) 1 << 31).

I have also found something unusual (but maybe this is done on purpose):
on the Microjet configuration, there is a periodic_telemetry_send_Fbw
function which is static inline; and contains a lot of static
variables. Which means that the variable will be duplicated in different
compilation units, which appears to happen in practice. But may this is
something that you want?

Best regards,
Matthieu Lemerre

Paparazzi-devel mailing list

reply via email to

[Prev in Thread] Current Thread [Next in Thread]