--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on February 2017 ---
I prefer starting with the command-line only, at least until all files are parsed, without running any analyses. You can save the result to a file e.g. via '-save parsed.sav', and then use '-load parsed.sav' to load it before doing analyses. Overall, this is my workflow: 1. frama-c [parse options] -save parsed.sav 2. frama-c -load parsed.sav [analysis options] Or, when using the GUI (for the second step only): 2. frama-c-gui -load parsed.sav I always save such commands in scripts/makefiles for future tuning and reproducibility. Also, I prefer using the GUI to inspect results, not so much to parameterize and run analyses. For Value in particular, due to the large amount of analysis options, a 3-step approach might be better: 1. frama-c [parse options] -save parsed.sav 2. frama-c -load parsed.sav [analysis options] -save value.sav 3. frama-c-gui -load value.sav On 03/02/2017 07:53, Prithvi Raj Narendra wrote: > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Ingénieur-chercheur CEA/LIST Laboratoire Sûreté et Sécurité des Logiciels -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170203/e9b10da8/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170203/e9b10da8/attachment-0001.bin>