anmaped / rmtld3synth

Runtime Verification toolchain for generation of monitors based on the restricted Metric Temporal Logic with Durations.
Other
6 stars 3 forks source link

Integrate monitor using rtmlib in a FreeRTOS context #2

Closed HenriqueMisson closed 1 year ago

HenriqueMisson commented 5 years ago

Hello,

I'm trying to integrate monitors using rtmlib in an embedded software based on FreeRTOS. I followed the steps written in the readme and I generated the folder "mon1" with the monitor and auxiliary functions.

I have changed the paths into Makefile in order to compile the mon1.cpp :

arm-monitor:
     arm-none-eabi-g++ -std=c++0x -march=armv7-m -g -fverbose-asm -O -Ihome/labvant/workspace/provant-software_RV/VANT_2.0/io-board/stm32f4/base/FreeRTOSV7.5.2/FreeRTOS/Source/include -Wframe-larger-than=1200 -DCONFIG_WCHAR_BUILTIN -Ihome/labvant/rmtld3synth/rtmlib/arch/arm/include/ -Ihome/labvant/rmtld3synth/rtmlib/ -DARM_CM4_FP -D__NUTTX__ --verbose -c mon1.cpp

And when I type make arm-mon, I get this error:

GGC heuristics: --param ggc-min-expand=100 --param ggc-min-heapsize=131072
ignoring duplicate directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/../../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include/c++/4.9.3"
ignoring duplicate directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/../../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include/c++/4.9.3/arm-none-eabi"
ignoring duplicate directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/../../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include/c++/4.9.3/backward"
ignoring duplicate directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/../../lib/gcc/arm-none-eabi/4.9.3/include"
ignoring nonexistent directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../arm-none-eabi/usr/local/include"
ignoring duplicate directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/../../lib/gcc/arm-none-eabi/4.9.3/include-fixed"
ignoring duplicate directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/../../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include"
ignoring nonexistent directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../arm-none-eabi/usr/include"
ignoring nonexistent directory "home/labvant/workspace/provant-software_RV/VANT_2.0/io-board/stm32f4/base/FreeRTOSV7.5.2/FreeRTOS/Source/include"
ignoring nonexistent directory "home/labvant/rmtld3synth/rtmlib/arch/arm/include/"
ignoring nonexistent directory "home/labvant/rmtld3synth/rtmlib/"
#include "..." search starts here:
#include <...> search starts here:
 /opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include/c++/4.9.3
 /opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include/c++/4.9.3/arm-none-eabi
 /opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include/c++/4.9.3/backward
 /opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/arm-none-eabi/4.9.3/include
 /opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/arm-none-eabi/4.9.3/include-fixed
 /opt/gcc-arm-none-eabi-4_9-2015q3/bin/../lib/gcc/arm-none-eabi/4.9.3/../../../../arm-none-eabi/include
End of search list.
mon1.cpp:1:0: error: target CPU does not support ARM mode
 #include "Mon0.h"
 ^
GNU C++ (GNU Tools for ARM Embedded Processors) version 4.9.3 20150529 (release) [ARM/embedded-4_9-branch revision 227977] (arm-none-eabi)
    compiled by GNU C version 4.7.4, GMP version 4.3.2, MPFR version 2.4.2, MPC version 0.8.1
GGC heuristics: --param ggc-min-expand=100 --param ggc-min-heapsize=131072
Makefile:13: recipe for target 'arm-monitor' failed
make: *** [arm-monitor] Error 1

I don't know why it says "ignoring nonexistent directory" and after reported an error.

This step is to compile the monitor before integrating that into my software. For the software I compile that with only "make" command to generate an .elf executable.

The toolchain that I'm using is the "arm-none-eabi", and to debug my code I use the "arm-none-eabi-gdb".

Could you help me in this sense?

Thanks.

anmaped commented 5 years ago

@HenriqueMisson Try to use the flag -marm (enables arm mode) or -mthumb (enables thumb mode). Try to use the correct -mtune=cortex-m4 since you are using the stm32f4.

HenriqueMisson commented 5 years ago

I inserted that into Makefile and also the path -Lhome/labvant/rmtld3synth/rtmlib/ and static library -llibrtml.a. But now I have the error which says that RTML_reader.h is not found ( RTML_reader.h: No such file or directory). I suppose that this was caused due the ignoring nonexistent directory:

ignoring nonexistent directory "/opt/gcc-arm-none-eabi-4_9-2015q3/bin/../arm-none-eabi/usr/include"
ignoring nonexistent directory "home/labvant/workspace/provant-software_RV/VANT_2.0/io-board/stm32f4/base/FreeRTOSV7.5.2/FreeRTOS/Source/include"
ignoring nonexistent directory "home/labvant/rmtld3synth/rtmlib/arch/arm/include/"
ignoring nonexistent directory "home/labvant/rmtld3synth/rtmlib/"

I searched about this error, however, none could help me.

anmaped commented 5 years ago

-L is for searching libraries. You have to use -I for the correct path of rtmlib.

I assume -I/home/labvant/rmtld3synth/rtmlib/

-I will include headers.

Another issue is that you forgot the root / in the path, and It's why is saying ignoring nonexistent directory.

Edit: When you use -l you should use the suffix of librtml.a without considering the library extension .a. The correct is -lrtml.

HenriqueMisson commented 5 years ago

I'm sorry, this it was my lack of attention.

Now, I need to adapt the the rtmlib to my FreeRTOS context, since the time_compat.h, used by many headers, calls the <nuttx/clock.h>. So due to this I could not finish the compilation.

Thank you Andre.

anmaped commented 5 years ago

@HenriqueMisson Yes. time and task compatible files should be some you may have to change. Everything else should work well.

anmaped commented 1 year ago

Version 0.4-alpha of rmtld3synth now includes support for rtmlib2, which in turn provides compatibility with FreeRTOS.