[Top][All Lists]

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

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

From: Felix Ruess
Subject: Re: [Paparazzi-devel] Source code analysis of paparazzi
Date: Wed, 5 Nov 2014 16:46:34 +0100

Hi Mathieu,

very nice, I'm sure we can put together a representative set of configurations (fixedwing, rotorcraft, lpc21, stm32f1/f4).
Any particular reason why you choose v5.0.5?
For us it would make a lot more sense if you could use the latest stable version v5.2

Regarding the LED macro, could you please tell us what compiler/toolchain you use?
I can't see where the (unsigned long) cast would come from, to me it looks like LED_INIT(4) should evaluate to something like

LED_DIR(4) |= _BV(LED_PIN(4))
IO_1_DIR |= _BV(31)

and with _BV from sw/include/std.h in (not resolving the io dir...)

IO_1_DIR |= (1 << (31))

which might still be wrong, but doesn't have the explicit cast and seemed to work (at least I could use LED_4 on my board...

Cheers, Felix

On Wed, Nov 5, 2014 at 4:25 PM, Karoly Molnar <address@hidden> wrote:
Hi Matthieu,

Do you mean that you would execute the formal verification of the paparazzi code base? It would propel the code quality of this autopilot well above any other available autopilot solutions!
I have checked Frama-C some times ago and think it is a very promising approach. I am just wondering if you would make the analysis framework available including all artifacts that would make then possible to repeat the analysis?
Do you plan to analyze the complete embedded code base including libopencm3? I do know that the latter is full of static analysis issues so it is very likely that you will detect many during the formal verification.


> From: address@hidden
> To: address@hidden
> Date: Wed, 5 Nov 2014 10:32:01 +0100
> Subject: [Paparazzi-devel] Source code analysis of paparazzi

> 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

reply via email to

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