Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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

[Frama-c-discuss] First time with Frama-C

  • Subject: [Frama-c-discuss] First time with Frama-C
  • From: prithvirajnarendra at gmail.com (Prithvi Raj Narendra)
  • Date: Fri, 3 Feb 2017 12:23:13 +0530
Greetings,
First of all thanks for the Open-source Frama-C tool. I came across it in
my search for a static analyser for the embedded projects that I work on.
My first issue is that with the GUI I'm not able to add any source files.
Whichever .c and/or .h file(s) I add I get 'Frama-C aborted: invalid user
input. Reverting to previous state. Look at the console for additional
information (if any).' error message. Is there something obviously wrong
that I'm doing?

I use arm gcc as the compiler. As usual the sequence is creating
dependencies and object files for every .c file and then linking them (the
command line for this is pasted below). How can I run Frama-C with command
line so that
1. the libc library of ARM GCC,
2. since there is an extern variable that is used in a bit of assembly
code, a single c source file complains of undefined reference. What is the
way to process multiple .c files? So that I can add this to the Makefile
too.

Cheers! Prithvi



arm-none-eabi-gcc -Os -ggdb3 -mcpu=cortex-m4 -mthumb -mabi=aapcs
-mfloat-abi=hard -mfpu=fpv4-sp-d16 --std=gnu11 -pedantic -Wall -Werror
-ffunction-sections -fdata-sections -fno-strict-aliasing -fno-builtin
--short-enums -flto -DDEBUG -DBLE_STACK_SUPPORT_REQD -DNRF52 -DNRF52832
-DBOARD_PCA10040 -DSOFTDEVICE_PRESENT -DS132 -DNRF52_PAN_64 -DNRF52_PAN_12
-DNRF52_PAN_58 -DNRF52_PAN_54 -DNRF52_PAN_31 -DNRF52_PAN_51 -DNRF52_PAN_36
-DNRF52_PAN_15 -DNRF52_PAN_20 -DNRF52_PAN_55 -DBLE_STACK_SUPPORT_REQD
-DCONFIG_NFCT_PINS_AS_GPIOS -DCONFIG_GPIO_AS_PINRESET
-DNRF_SD_BLE_API_VERSION=3  -DSWI_DISABLE0  -I. -I../../platform
-I../../SDK_components/drivers_nrf/delay -I../../SDK_components/drivers_nrf/hal
-I../../SDK_components/device -I../../SDK_components/toolchain
-I../../SDK_components/toolchain/cmsis/include
-I/usr/arm-none-eabi/include/ -M main.c -MF "obj/main.d" -MT obj/main.o
arm-none-eabi-gcc -Os -ggdb3 -mcpu=cortex-m4 -mthumb -mabi=aapcs
-mfloat-abi=hard -mfpu=fpv4-sp-d16 --std=gnu11 -pedantic -Wall -Werror
-ffunction-sections -fdata-sections -fno-strict-aliasing -fno-builtin
--short-enums -flto -DDEBUG -DBLE_STACK_SUPPORT_REQD -DNRF52 -DNRF52832
-DBOARD_PCA10040 -DSOFTDEVICE_PRESENT -DS132 -DNRF52_PAN_64 -DNRF52_PAN_12
-DNRF52_PAN_58 -DNRF52_PAN_54 -DNRF52_PAN_31 -DNRF52_PAN_51 -DNRF52_PAN_36
-DNRF52_PAN_15 -DNRF52_PAN_20 -DNRF52_PAN_55 -DBLE_STACK_SUPPORT_REQD
-DCONFIG_NFCT_PINS_AS_GPIOS -DCONFIG_GPIO_AS_PINRESET
-DNRF_SD_BLE_API_VERSION=3  -DSWI_DISABLE0  -I. -I../../platform
-I../../SDK_components/drivers_nrf/delay -I../../SDK_components/drivers_nrf/hal
-I../../SDK_components/device -I../../SDK_components/toolchain
-I../../SDK_components/toolchain/cmsis/include
-I/usr/arm-none-eabi/include/ -c -o obj/main.o main.c

arm-none-eabi-gcc -Os -ggdb3 -mcpu=cortex-m4 -mthumb -mabi=aapcs
-mfloat-abi=hard -mfpu=fpv4-sp-d16 --std=gnu11 -pedantic -Wall -Werror
-ffunction-sections -fdata-sections -fno-strict-aliasing -fno-builtin
--short-enums -flto -DDEBUG -DBLE_STACK_SUPPORT_REQD -DNRF52 -DNRF52832
-DBOARD_PCA10040 -DSOFTDEVICE_PRESENT -DS132 -DNRF52_PAN_64 -DNRF52_PAN_12
-DNRF52_PAN_58 -DNRF52_PAN_54 -DNRF52_PAN_31 -DNRF52_PAN_51 -DNRF52_PAN_36
-DNRF52_PAN_15 -DNRF52_PAN_20 -DNRF52_PAN_55 -DBLE_STACK_SUPPORT_REQD
-DCONFIG_NFCT_PINS_AS_GPIOS -DCONFIG_GPIO_AS_PINRESET
-DNRF_SD_BLE_API_VERSION=3  -DSWI_DISABLE0  -I. -I../../platform
-I../../SDK_components/drivers_nrf/delay -I../../SDK_components/drivers_nrf/hal
-I../../SDK_components/device -I../../SDK_components/toolchain
-I../../SDK_components/toolchain/cmsis/include
-I/usr/arm-none-eabi/include/ -M ../../SDK_components/toolchain/system_nrf52.c
-MF "obj/system_nrf52.d" -MT obj/system_nrf52.o
arm-none-eabi-gcc -Os -ggdb3 -mcpu=cortex-m4 -mthumb -mabi=aapcs
-mfloat-abi=hard -mfpu=fpv4-sp-d16 --std=gnu11 -pedantic -Wall -Werror
-ffunction-sections -fdata-sections -fno-strict-aliasing -fno-builtin
--short-enums -flto -DDEBUG -DBLE_STACK_SUPPORT_REQD -DNRF52 -DNRF52832
-DBOARD_PCA10040 -DSOFTDEVICE_PRESENT -DS132 -DNRF52_PAN_64 -DNRF52_PAN_12
-DNRF52_PAN_58 -DNRF52_PAN_54 -DNRF52_PAN_31 -DNRF52_PAN_51 -DNRF52_PAN_36
-DNRF52_PAN_15 -DNRF52_PAN_20 -DNRF52_PAN_55 -DBLE_STACK_SUPPORT_REQD
-DCONFIG_NFCT_PINS_AS_GPIOS -DCONFIG_GPIO_AS_PINRESET
-DNRF_SD_BLE_API_VERSION=3  -DSWI_DISABLE0  -I. -I../../platform
-I../../SDK_components/drivers_nrf/delay -I../../SDK_components/drivers_nrf/hal
-I../../SDK_components/device -I../../SDK_components/toolchain
-I../../SDK_components/toolchain/cmsis/include
-I/usr/arm-none-eabi/include/ -c -o obj/system_nrf52.o ../../SDK_components/
toolchain/system_nrf52.c

Compiling:  ../../SDK_components/toolchain/gcc/gcc_startup_nrf52.S
arm-none-eabi-gcc -Os -ggdb3 -mcpu=cortex-m4 -mthumb -mabi=aapcs
-mfloat-abi=hard -mfpu=fpv4-sp-d16 --std=gnu11 -pedantic -Wall -Werror
-ffunction-sections -fdata-sections -fno-strict-aliasing -fno-builtin
--short-enums -flto -DDEBUG -DBLE_STACK_SUPPORT_REQD -DNRF52 -DNRF52832
-DBOARD_PCA10040 -DSOFTDEVICE_PRESENT -DS132 -DNRF52_PAN_64 -DNRF52_PAN_12
-DNRF52_PAN_58 -DNRF52_PAN_54 -DNRF52_PAN_31 -DNRF52_PAN_51 -DNRF52_PAN_36
-DNRF52_PAN_15 -DNRF52_PAN_20 -DNRF52_PAN_55 -DBLE_STACK_SUPPORT_REQD
-DCONFIG_NFCT_PINS_AS_GPIOS -DCONFIG_GPIO_AS_PINRESET
-DNRF_SD_BLE_API_VERSION=3  -DSWI_DISABLE0  -I. -I../../platform
-I../../SDK_components/drivers_nrf/delay -I../../SDK_components/drivers_nrf/hal
-I../../SDK_components/device -I../../SDK_components/toolchain
-I../../SDK_components/toolchain/cmsis/include
-I/usr/arm-none-eabi/include/ -c -o obj/gcc_startup_nrf52.o
../../SDK_components/toolchain/gcc/gcc_startup_nrf52.S

arm-none-eabi-gcc -Xlinker -Map=build/hello_world_blinky.map
--specs=nano.specs -lc -lnosys -mcpu=cortex-m4  -mthumb  -mabi=aapcs
-mfloat-abi=hard -mfpu=fpv4-sp-d16 -T../../SDK_components/
softdevice/s132/toolchain/armgcc/armgcc_s132_nrf52832_xxaa.ld
-Wl,--gc-sections -flto
-L../../SDK_components/softdevice/s132/toolchain/armgcc/
-L../../SDK_components/toolchain/gcc/ obj/main.o obj/system_nrf52.o
obj/gcc_startup_nrf52.o -o build/hello_world_blinky.elf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170203/64168f44/attachment.html>