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: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Fri, 3 Feb 2017 13:53:39 +0100
  • In-reply-to: <CALu-FW04tRVNo9Amki=T2YbkN6qJRcPyAiGgFQLtmM1dQ_fQtw@mail.gmail.com>
  • References: <CALu-FW04tRVNo9Amki=T2YbkN6qJRcPyAiGgFQLtmM1dQ_fQtw@mail.gmail.com>
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>