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

[Matthieu Lemerre]

Hello,

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
welcome!

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

Regards,
Matthieu


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 http://verigames.com/). 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
>> https://lists.nongnu.org/mailman/listinfo/paparazzi-devel
>
>
> _______________________________________________
> Paparazzi-devel mailing list
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/paparazzi-devel