diff options
author | jaseg <git@jaseg.de> | 2021-03-02 19:27:52 +0100 |
---|---|---|
committer | jaseg <git@jaseg.de> | 2021-03-02 19:27:52 +0100 |
commit | b328ef60595523e3922aae994d7bbe06c7c3fa56 (patch) | |
tree | bdbbd1a4a0528d6f479f903fbd1f1c04476ec5fe /fw/src/frama_c_cmdline | |
parent | 6eddc61626d470363ba464c57a5fc5ec7e8ce329 (diff) | |
parent | 5b94dee9cfb1eaaf28510b843c60355663b660ea (diff) | |
download | secure-hid-b328ef60595523e3922aae994d7bbe06c7c3fa56.tar.gz secure-hid-b328ef60595523e3922aae994d7bbe06c7c3fa56.tar.bz2 secure-hid-b328ef60595523e3922aae994d7bbe06c7c3fa56.zip |
Add 'fw/' from commit '5b94dee9cfb1eaaf28510b843c60355663b660ea'
git-subtree-dir: fw
git-subtree-mainline: 6eddc61626d470363ba464c57a5fc5ec7e8ce329
git-subtree-split: 5b94dee9cfb1eaaf28510b843c60355663b660ea
Diffstat (limited to 'fw/src/frama_c_cmdline')
-rw-r--r-- | fw/src/frama_c_cmdline | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/fw/src/frama_c_cmdline b/fw/src/frama_c_cmdline new file mode 100644 index 0000000..d6c6adc --- /dev/null +++ b/fw/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 |