summaryrefslogtreecommitdiff
path: root/src/frama_c_cmdline
diff options
context:
space:
mode:
authorjaseg <git@jaseg.net>2018-12-17 12:26:51 +0900
committerjaseg <git@jaseg.net>2018-12-17 12:26:51 +0900
commit40e9fb8153a218a243cff749d7d0b4e82d70ae94 (patch)
tree831254a0d04a45012d5f11bb5f581833a95ae177 /src/frama_c_cmdline
parenteb3b3b884c0e119f40499019277e984988502dbe (diff)
downloadsecure-hid-40e9fb8153a218a243cff749d7d0b4e82d70ae94.tar.gz
secure-hid-40e9fb8153a218a243cff749d7d0b4e82d70ae94.tar.bz2
secure-hid-40e9fb8153a218a243cff749d7d0b4e82d70ae94.zip
Invocation of noise.c from demo.c mostly proving in frama-c
Diffstat (limited to 'src/frama_c_cmdline')
-rw-r--r--src/frama_c_cmdline1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/frama_c_cmdline b/src/frama_c_cmdline
new file mode 100644
index 0000000..d6c6adc
--- /dev/null
+++ b/src/frama_c_cmdline
@@ -0,0 +1 @@
+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