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

[Matthieu Lemerre]

Hi Felix and Karoly,

Yes, this was a configuration error from my side, the code is
correct. The long that appear is in the source code after being parsed
by Frama-C; the problem I had here is that I forgot to configure the
Frama-C libc emulation correctly, and it translated int64_t to long
instead of long long.

@Karoly: Keep in mind that this is source code analysis, so there is no
compiler settings outside of configuration of Frama-C itself... 

Best regards,
Matthieu

Felix Ruess <address@hidden> writes:

> Hi Matthieu,
>
> I can't reproduce the issue.
>
> Seems like your parser adds the (long) casts as that is nowhere in our code:
> #define INT32_RAD_OF_DEG(_deg) (int32_t)(((int64_t)(_deg) *
> 14964008)/857374503)
>
> So this looks good to me as you should be able to pass up to 61637 degrees
> to that function...
> Maximum you can pass before intermediate multiplication overflows:
> pow(2,63) / 14964008 = 616370429423 in deg*1e7= 61637 in deg
>
> Cheers, Felix
>
> On Wed, Nov 26, 2014 at 4:53 PM, Matthieu Lemerre <address@hidden>
> wrote:
>
>>
>> Hi Felix,
>>
>> Thanks for the list of configurations. I have began the analysis of the
>> Quad_LisaM_2 target, and I found the following bug: in ins_int.c, the
>> ins_init function does:
>>
>> llh_nav0.lat = INT32_RAD_OF_DEG(NAV_LAT0);
>>
>> The macro expansion of which gives (If I configured things correctly):
>>
>> llh_nav0.lat = (int)(((long)435641194 * (long)14964008) / (long)857374503);
>>
>> The intermediate calculation (long) 435641194 * (long)14964008 causes an
>> overflow, and may not be compiled correctly.
>>
>> A work-around is to produce this code instead:
>>
>> int j = ((435641194ULL * 14964008ULL) / 857374503ULL);
>>
>> The intermediary computation fits in 64bit, and this solve the problem
>> here. However, I don't know a general solution to this problem if you
>> had a constant expression which required an intermediate computation
>> that does not fit in 64bit, I would be interested to know if you could
>> find one.
>>
>> Cheers,
>> Matthieu
>>
>> Felix Ruess <address@hidden> writes:
>>
>> > Hi Matthieu,
>> >
>> > If you want only two examples, I would suggest the following aircrafts
>> from
>> > the example conf:
>> > - rotorcraft, stm32f1: Quad_LisaM_2
>> > - fixedwing, lpc21: Microjet
>> >
>> > Of course these only represent a small subset of Paprazzi...
>> >
>> > Cheers, Felix
>> >
>> > On Fri, Nov 21, 2014 at 4:48 PM, Matthieu Lemerre <
>> address@hidden>
>> > wrote:
>> >
>> >>
>> >> Hi Michal,
>> >>
>> >> Thanks. Actually, a single-threaded mainloop is simpler to analyze, so
>> >> I'll stick with that for the moment.
>> >>
>> >> However, I would still be interested if you could give me the name of 2
>> >> configurations that are different in both dimensions {fixedwing,
>> >> rotorcraft} and {lpc2148,stm32}.
>> >>
>> >> Thanks,
>> >> Matthieu
>> >>
>> >>
>> >> Michal Podhradsky <address@hidden> writes:
>> >>
>> >> > Hi Matthieu,
>> >> >
>> >> > I am really glad that you are analysing Paparazzi code. There is an
>> >> > experimental branch based on RTOS ChibiOS, current version can be
>> found
>> >> > here: https://github.com/paparazzi/paparazzi/tree/rt_paparazzi
>> >> > It  contains working configuration for Rotorcraft & Lisa M/MX. There
>> are
>> >> > around 13 threads running for various subsystems, plus mutexes etc. so
>> >> you
>> >> > might find it interesting to analyse multi-threaded version of
>> Paparazzi.
>> >> >
>> >> > Regards
>> >> > Michal
>> >> >
>> >> > On Thu, Nov 6, 2014 at 1:59 AM, Alexandre Bustico <
>> >> > address@hidden> wrote:
>> >> >
>> >> >> Le 06/11/2014 10:38, Matthieu Lemerre a écrit :
>> >> >>
>> >> >>> it seems that the generated source code is single-threaded, but
>> >> >>> are there other threads?
>> >> >>>
>> >> >>
>> >> >> In the master branch, there  is single-threaded mainloop, but many
>> >> >> callbacks are interrupt driven,
>> >> >> from hardware timer, and all the peripherals (i2c, spi, dma, uart,
>> etc
>> >> >> etc).
>> >> >>
>> >> >> there is also in another branch an experimental rtos (chibios)
>> version
>> >> >> which use threads.
>> >> >>
>> >> >> --
>> >> >> Alexandre
>> >> >>
>> >> >>
>> >> >>
>> >> >> _______________________________________________
>> >> >> 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
>> >>
>> >> _______________________________________________
>> >> 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
>>