#!/bin/bash

# ivette 是 frama-c 的 GUI 工具，若使用 GUI 模式，请使用 ivette 命令替换 frama-c 命令。

frama-c -wp \
  -rte \
  verify_sm4/crypt_sm4.c \
  -wp-timeout 10 \
  -wp-split  \
  -wp-out ./_wp_out_sm4 \
  -wp-par 4 \
  -wp-prover z3, alt-ergo \
  -cpp-extra-args=" \
    -DHITLS_CRYPTO_SM4  \
    -I ../openhitls/config  \
    -I ../openhitls/config/macro_config \
    -I ../openhitls/crypto/include \
    -I ../openhitls/crypto/sm4/include \
    -I ../openhitls/include \
    -I ../openhitls/include/bsl \
    -I ../openhitls/include/crypto \
    -I ../openhitls/include/bsl/err/include \
    -I ../openhitls/platform/Secure_C/include"  


# -wp: 启用WP插件
# -eva: 启用EVA插件
# -rte: 检查运行时错误
# -wp-out: 指定WP输出目录
# -wp-par: 使用k个并行进程进行验证
# -wp-timeout: 设置每个证明任务的超时时间(秒)，默认10秒
# -wp-steps: 设置SMT求解器的最大步数，默认值较小，这里设为50000
# -wp-prover: 指定使用的自动定理证明器
# -wp-split: 启用分割VC以提高证明效率
# -cpp-extra-args="...": 传递给C预处理器的额外参数，包括宏定义和包含路径