[Top][All Lists]

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

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

From: Matthieu Lemerre
Subject: Re: [Paparazzi-devel] Source code analysis of paparazzi
Date: Wed, 05 Nov 2014 11:25:18 +0100
User-agent: Notmuch/0.15.2 ( Emacs/24.3.1 (x86_64-pc-linux-gnu)


I'm currently running v5.0.5_stable. I was planning to try to run all of
the configurations (this would create more instances for the game), but
your advice on which configurations to focus the verification efforts is

I think the people that you have met are former colleagues that have
left CEA.


Gautier Hattenberger <address@hidden> writes:

> Hello,
> 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 ?
> Regards
> Gautier Hattenberger
> Le 05/11/2014 10:32, Matthieu Lemerre a écrit :
>> Hello,
>> 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
>> address@hidden
> _______________________________________________
> Paparazzi-devel mailing list
> address@hidden

reply via email to

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