Bitcraze Forums

Hello everyone, During a 6 months internship at AdaCore, I reimplemented the Crazyflie firmware using SPARK, a technology based on formal methods used to prove code correctness. Here is a link to a previous topic where I presented the work I was doing: https://forum.bitcraze.io/viewtopic.php?f=6&...

Hello Bitcraze community

I've done a blog post explaining all the work I've been doing on the Crazyflie firmware using SPARK on the AdaCore Blog.

For those who are interested, here is the link: http://blog.adacore.com/how-to-prevent- ... sing-spark

Enjoy

I forgot to mention that I didn't rewrite the LOG/Param subsystem yet: thus, I don't send the TOC to the python client when starting. I don't know if it's mandatory for the client to get the TOC at start...

Thanks in advance for your answers

Hello everyone! I have translated the whole CRTP communication protocol in Ada and I'm receiving radio packets in the CRTP_PORT_LINK. The crtpservice module seems to handle a sort of acknowledgement between the Crazyflie and the python client, and the packet channel seems to determine what response ...

Hello everyone, I want to implement the Crazyflie LOG subsystem in ADA. I'm trying to figure out how it works in log.h and log.c. I see that the macros used to register Log groups with the variables to be logged (LOG_GROUP_START, LOG_GROUP_STOP) puts all the 'log_s' structures (containing the type, ...

Yes exactly and you would be able to see this in the console output when "<F>" is displayed.

Ok, I see how the things work now.

Thank you for your answers

Ok I see. But nothing is done to recover from this situation, right?

So if many calls to 'consolePuts' (via DEBUG_PRINT) are done during startup, when the CF is not yet connected, some of these messages will never be sent to the client python, am I right?

Nobody can help?

Hi everybody, I'm currently trying to translate the Crazyflie 2.0 firmware in ADA. Looking deeper in the code, I don't understand this piece of code, located in console.c: static const char fullMsg[] = "<F>\n"; // ... int consolePutchar(int ch) { int i; // ... if (ch == '\n' || messageToPr...

Well I understant that you want to "convert" the Syslink packet into a CRTPPacket by "filling" the CRTPPacket with the Sysling length (previously decreased, to remove the 'type' component of the Syslink packet). But the problem is that the size of the CRTPPacket struct is 32 byte...