c - 欧洲航天局考虑使用 Frama-C;需要帮助
问题描述
Frama-C 社区。我的名字是 Maurizio Martignano (www.spazioit.com)。
我为 ESA 任务执行独立的软件验证和验证,目前正在参与欧洲航天局的一个项目,该项目试图收集一组静态分析工具,并以预先打包的即用型形式提供,用于“盲" 分析 - 即按原样查看代码(没有任何类型的特定于分析器的注释)。
我不确定 Frama-C 是否适合这个模型——我对开源代码库的初步结果似乎证实了该工具不能与“原样”代码库一起使用。
这就是我所做的...
我将 Crazyflie 系统作为测试平台:https ://github.com/bitcraze/crazyflie-firmware 。
它的构建工具集可在此处获得:https ://launchpad.net/gcc-arm-embedded/+download 。
从 Makefile,我构建了以下脚本 (frama-c-abalyze.sh),它应该从“src”文件夹中调用。
#frama-c -c11 -kernel-msg-key pp -kernel-warn-error=-annot-error -cpp-extra-args="-DUSE_RADIOLINK_CRTP -DENABLE_UART -DARM_MATH_CM4 -D__FPU_PRESENT=1 -D__TARGET_FPU_VFP -DBOARD_REV_D -DESTIMATOR_NAME=anyEstimator -DCONTROLLER_NAME=ControllerTypeAny -DPOWER_DISTRIBUTION_TYPE_stock -Ilib/FreeRTOS/include -Ilib/FreeRTOS/portable/GCC/ARM_CM4F -Isrc -Iconfig -Ihal/interface -Imodules/interface -Iutils/interface -Idrivers/interface -Iplatform -I../vendor/CMSIS/CMSIS/Include -Idrivers/bosch/interface -Ilib/STM32F4xx_StdPeriph_Driver/inc -Ilib/CMSIS/STM32F4xx/Include -Ilib/STM32_USB_Device_Library/Core/inc -Ilib/STM32_USB_OTG_Driver/inc -Ideck/interface -Ideck/drivers/interface -Iutils/interface/clockCorrection -Iutils/interface/tdoa -Iutils/interface/lighthouse -I../vendor/libdw1000/inc -Ilib/FatFS -Ilib/vl53l1 -Ilib/vl53l1/core/inc -DSTM32F4XX -DSTM32F40_41xxx -DHSE_VALUE=8000000 -DUSE_STDPERIPH_DRIVER" $*
frama-c -c11 -kernel-msg-key pp -kernel-warn-error=-annot-error -no-cpp-frama-c-compliant -no-frama-c-stdlib -cpp-command="arm-none-eabi-gcc -E -DUSE_RADIOLINK_CRTP -DENABLE_UART -DARM_MATH_CM4 -D__FPU_PRESENT=1 -D__TARGET_FPU_VFP -DBOARD_REV_D -DESTIMATOR_NAME=anyEstimator -DCONTROLLER_NAME=ControllerTypeAny -DPOWER_DISTRIBUTION_TYPE_stock -mcpu=cortex-m4 -mthumb -mfloat-abi=hard -mfpu=fpv4-sp-d16 -Ilib/FreeRTOS/include -Ilib/FreeRTOS/portable/GCC/ARM_CM4F -Isrc -Iconfig -Ihal/interface -Imodules/interface -Iutils/interface -Idrivers/interface -Iplatform -I../vendor/CMSIS/CMSIS/Include -Idrivers/bosch/interface -Ilib/STM32F4xx_StdPeriph_Driver/inc -Ilib/CMSIS/STM32F4xx/Include -Ilib/STM32_USB_Device_Library/Core/inc -Ilib/STM32_USB_OTG_Driver/inc -Ideck/interface -Ideck/drivers/interface -Iutils/interface/clockCorrection -Iutils/interface/tdoa -Iutils/interface/lighthouse -I../vendor/libdw1000/inc -Ilib/FatFS -Ilib/vl53l1 -Ilib/vl53l1/core/inc -DSTM32F4XX -DSTM32F40_41xxx -DHSE_VALUE=8000000 -DUSE_STDPERIPH_DRIVER %1 > %2" $*
第一行调用带有自己的包含文件和预处理器的 Frama-C。第二行调用 Frama-C,构建系统包含文件和预处理器。
使用第二行并将其应用于“src”文件夹中的所有 *.c 文件,这些文件也出现在 Makefile 中,我得到了许多 Frama-C“编译错误”,例如“语法错误”、“无效的用户输入”、“用户错误”。
最重要的是,我尝试在没有显示任何“编译”错误的文件上调用“val”插件,例如“./modules/src/log.c”。我使用了如下命令:
./frama-c-analyze.sh -rte -val -main logTask modules/src/log.c
./frama-c-analyze.sh -rte -val -main logTOCProcess modules/src/log.c
./frama-c-analyze.sh -rte -val -main logControlProcess modules/src/log.c
将这种类型的命令应用于文件中的所有函数。
我设法得到的输出如下所示:
[value:alarm] modules/src/log.c:771: Warning:
assertion 'rte,mem_access' got status unknown.
[value:alarm] modules/src/log.c:771: Warning:
out of bounds read. assert \valid_read(&ops->variable);
[value:alarm] modules/src/log.c:772: Warning:
我发现这种类型的输出信息量不大,而且有点误报。
我做错什么了吗?我错过了什么吗?我是否需要使用 Frama-C 包含并使用 ACLS 注释“丰富”代码?
非常感谢你,毛里齐奥
解决方案
推荐阅读
- coredump - exec查询cmd时的Greenplum coredump
- python - 查找使用列表表示的所有组合
- java - 如何修复“org.hibernate.boot.registry.selector.spi.StrategySelectionException:无法解析名称 [org.hibernate.dialect.MySQL8Dialect]”?
- python - 如何更改列表中文件的文件扩展名
- python - 进化算法的正则表达式语法结构
- python-3.x - 面向对象编程类和模块之间的区别
- java - 将 @OneToMany 关系与主键映射为外键
- java - Eclipse:触发完全重建
- javascript - 如何通过 id 获取 span 元素?
- javascript - 如何使用插入到 Javascript 中的 SQLite 列中的值?