#!/bin/bash

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

frama-c -wp \
    verify_sm4/sm4cfb.c \
    verify_sm4/crypt_sm4.h \
    verify_sm4/noasm_sm4_cfb.c \
    verify_sm4/crypt_sm4_public.c \
    verify_sm4/crypt_sm4.c \
    verify_sm4/sm4_key.c \
    verify_sm4/crypt_modes_cfb.h \
    verify_sm4/modes_cfb.c \
    -wp-out ./_wp_out_sm4_cfb \
    -wp-par 4 \
    -wp-timeout 10\
    -wp-prover "z3, alt-ergo" \
    -cpp-extra-args="\
        -DHITLS_CRYPTO_SM4 \
        -DHITLS_CRYPTO_CFB \
        -DHITLS_CRYPTO_MODES \
        -I ../openhitls/bsl/err/include \
        -I ../openhitls/include \
        -I ../openhitls/include/bsl \
        -I ../openhitls/include/crypto \
        -I ../openhitls/config \
        -I ../openhitls/config/macro_config \
        -I ../openhitls/crypto/eal/src \
        -I ../openhitls/crypto/include \
        -I ../openhitls/crypto/modes/include \
        -I ../openhitls/crypto/modes/src \
        -I ../openhitls/crypto/sm4/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预处理器的额外参数，包括宏定义和包含路径