--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on February 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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>