diff options
Diffstat (limited to 'src/frama_c_cmdline')
| -rw-r--r-- | src/frama_c_cmdline | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/frama_c_cmdline b/src/frama_c_cmdline deleted file mode 100644 index d6c6adc..0000000 --- a/src/frama_c_cmdline +++ /dev/null @@ -1 +0,0 @@ -frama-c-gui -c11 -cpp-extra-args="-DVERIFICATION -DSTM32F4 -DUSE_STM32F4_USBH_DRIVER_FS -DDEBUG_USART=USART1 -DDEBUG_USART_BAUDRATE=115200 -DDEBUG_USART_DMA_CHANNEL_NUM=4 -DDEBUG_USART_DMA_NUM=2 -DDEBUG_USART_DMA_STREAM_NUM=7 -I. -I"(frama-c -print-path)"/libc -I crypto/noise-c/include -I../include -I../libopencm3/include" -wp -wp-rte -wp-model +cint -wp-verbose 2 -slevel 8 -wp-out goals noise.c demo.c -wp-fct try_continue_noise_handshake |