Frama-C多函数调用与静态变量的规格验证技术问询

我正在探索Frama-C的核心功能，尤其是WP（最弱前置条件）和Value分析工具，最终目的是把这些工具应用到大型多层代码上——这类代码有几个典型特征：

• 包含大量嵌套函数调用
• 使用复杂的数据结构
• 依赖静态及/或全局变量

当前分析方法与遇到的问题 #

目前我采用自底向上的分析策略：先用-lib-entry和-main内核选项隔离出没有外部函数调用的独立函数，给它们定义行为规格并完成分析，确保只要前置条件满足，函数契约就能被验证。但当我开始给调用下层函数的上层函数写规格时，麻烦就来了：我经常需要为被调用的下层函数明确行为，可这些函数可能涉及当前函数作用域之外的变量或其他函数。

简化示例场景 #

为了说明问题，我准备了一个简化的例子：

• 在file1.h中定义了包含number和parity字段的结构体my_struct
• 在file1.c中有两个函数：
  • check_parity：检查静态变量_sVar的parity字段是否正确
  • correct_parity：调用check_parity，若parity字段不正确则修正它
• 在file2.c中有函数outside_caller，仅调用correct_parity()，我的目标是为outside_caller完成与correct_parity一致的规格定义。

file1.h #

/* parity = 0 => even ; 1 => odd */
typedef unsigned char TYP_U08;
typedef unsigned short TYP_U16;
typedef unsigned int TYP_U32;
typedef unsigned long TYP_U64;

typedef struct {
    unsigned char parity;
    unsigned int number;
} my_stuct;

typedef enum {
    S_ERROR = -1,
    S_OK = 0,
    S_WARNING = 1
} TYPE_STATUS;

/*@ ghost my_stuct* g_sVar; */

/*@ predicate fc_pre_is_parity_ok{Labl}(my_stuct* i_sVar) = (
    \at(i_sVar->parity, Labl) == ((TYP_U08) (\at(i_sVar->number,Labl) % 2u))
);

@ predicate fc_pre_valid_parity{Labl}(my_stuct* i_sVar) = (
    (\at(i_sVar->parity,Labl) == 0) || (\at(i_sVar->parity, Labl) == 1)
);

@ predicate fc_pre_is_parity_readable(my_stuct* i_sVar) = (
    \valid_read(&i_sVar->parity)
);

@ predicate fc_pre_is_parity_writeable(my_stuct* i_sVar) = (
    \valid(&i_sVar->parity)
);

@ predicate fc_pre_is_number_readable(my_stuct* i_sVar) = (
    \valid_read(&i_sVar->number)
);

@ predicate fc_pre_is_number_writeable(my_stuct* i_sVar) = (
    \valid(&i_sVar->number)
);
*/

TYPE_STATUS check_parity(void);
TYPE_STATUS correct_parity(void);

file1.c #

static my_stuct* _sVar;

/*@ requires check_req_parity_readable: fc_pre_is_parity_readable(_sVar);
  @ requires check_req_number_readable: fc_pre_is_number_readable(_sVar);
  @ assigns check_assigns: g_sVar;
  @ ensures check_ensures_error: !fc_pre_valid_parity{Post}(g_sVar) ==> \result == S_ERROR;
  @ ensures check_ensures_ok: ( fc_pre_valid_parity{Post}(g_sVar) && fc_pre_is_parity_ok{Post}(g_sVar) ) ==> \result == S_OK;
  @ ensures check_ensures_warning: ( fc_pre_valid_parity{Post}(g_sVar) && !fc_pre_is_parity_ok{Post}(g_sVar) ) ==> \result == S_WARNING;
  @ ensures check_ensures_ghost_consistency: \at(g_sVar, Post) == _sVar;
*/
TYPE_STATUS check_parity(void) {
    //@ ghost g_sVar = _sVar;
    TYPE_STATUS status = S_OK;
    if(!(_sVar->parity == 0 || _sVar->parity == 1)) {
        status = S_ERROR;
    } else if ( _sVar->parity == (TYP_U08)(_sVar->number % 2u) ){
        status = S_OK;
    } else {
        status = S_WARNING;
    }
    return status;
}

/*@ requires correct_req_is_parity_writeable: fc_pre_is_parity_writeable(_sVar);
  @ requires correct_req_is_number_readable: fc_pre_is_number_readable(_sVar);
  @ assigns correct_assigns: _sVar->parity, g_sVar, g_sVar->parity;
  @ ensures correct_ensures_error: !fc_pre_valid_parity{Pre}(g_sVar) ==> \result == S_ERROR;
  @ ensures correct_ensures_ok: ( fc_pre_valid_parity{Pre}(g_sVar) && fc_pre_is_parity_ok{Pre}(g_sVar) ) ==> \result == S_OK;
  @ ensures correct_ensures_warning: ( fc_pre_valid_parity{Pre}(g_sVar) && !fc_pre_is_parity_ok{Pre}(g_sVar) ) ==> \result == S_WARNING;
  @ ensures correct_ensures_consistency: fc_pre_is_parity_ok{Post}(g_sVar);
  @ ensures correct_ensures_validity : fc_pre_valid_parity{Post}(g_sVar);
  @ ensures correct_ensures_ghost_consistency: \at(g_sVar, Post) == _sVar;
*/
TYPE_STATUS correct_parity(void) {
    //@ ghost g_sVar = _sVar;
    TYPE_STATUS parity_status = check_parity();
    if(parity_status == S_ERROR || parity_status == S_WARNING) {
        _sVar->parity = (TYP_U08)(_sVar->number % 2u);
        /*@ assert (\at(g_sVar->parity,Here) == 0) || (\at(g_sVar->parity, Here) == 1);

内容的提问来源于stack exchange，提问作者Eliott.CH