Frama-C处理_Bool值时触发意外断言失败错误的技术问询

使用Frama-C 25.0-beta（Manganese）版本执行命令frama-c -deps -eva test.c分析以下代码时，触发src/kernel_services/abstract_interp/offsetmap.ml第945行的断言失败：

_Bool get_bool(void){ return (_Bool)1; };
_Bool pass_bool(_Bool b){ return b; };

_Bool b_flag1, b_flag2;

int main(){
    b_flag1 = pass_bool( !((_Bool) get_bool()) );
    b_flag2 = pass_bool( (_Bool) get_bool() );
}

已知规避方法 #

• 仅保留main中任意一行赋值代码（注释掉另一行）
• 移除pass_bool调用中的(_Bool)强制类型转换
• 先用临时变量存储get_bool()的返回值，再传入pass_bool
• 移除get_bool()返回值的取反操作

解决方案与提示 #

这是Frama-C EVA分析器在处理_Bool类型复合嵌套操作（强制转换+取反+函数调用）时的版本特定bug。可行的解决路径：

1. 升级到稳定版本：Beta版本本身存在未修复的问题，建议升级到Manganese正式版（25.0）或更高版本，这类底层断言失败问题通常会在正式发布前被修复。
2. 使用规避写法：采用你已经发现的任意一种规避方式，优先推荐用临时变量拆分嵌套操作，既能规避bug，也能提升代码可读性。
3. 提交bug反馈：如果升级稳定版后问题仍存在，可以向Frama-C开发团队提交bug报告，附上测试代码和完整错误信息，帮助定位修复。

内容的提问来源于stack exchange，提问作者Gruber