Frama-C是否支持GNU C定点算术扩展？嵌入式代码验证遇语法错误

问题场景 #

我正在结合Frama-C与MPLAB做微控制器嵌入式代码验证，完成编译器适配后，遇到Frama-C无法识别GNU C定点类型_Fract的语法错误，具体报错如下：

syntax error:
Location: line 28, between columns 15 and 16, before or at token: _Fract
26
27        typedef CHANNEL_TYPE Channel_t;
28        typedef XXXX_TYPE Xxxx_t;
                       ^

代码中的宏定义为：

#define XXXX_TYPE          sat fract 

注：fract是_Fract的宏别名。

我的核心需求：可以将定点类型当作普通整数处理，但希望尽可能不修改原有业务代码。

环境信息：

• Frama-C版本：31.0 (Gallium)
• 编译器：gcc version 8.3.1 (Microchip XC32 Compiler v4.21)

可行解决方案 #

1. 预处理宏直接替换（最简方案） #

调用Frama-C时添加预处理参数，强制将_Fract、fract和sat替换为Frama-C能识别的内容，无需改动源码：

frama-c -D _Fract=int -D fract=int -D sat= [你的源文件路径]

解释：

• -D _Fract=int和-D fract=int把定点类型直接映射为普通整数
• -D sat=空替换sat关键字（因为Frama-C不支持该修饰符，且我们已将类型转成整数，饱和语义可后续用ACSL断言补充）

2. 映射为带约束的整数（保留部分语义） #

如果需要保留定点类型的取值范围约束，可通过Frama-C的ACSL注解间接实现，无需修改源码：

1. 先通过预处理宏把_Fract替换为带属性的整数：

frama-c -D _Fract='int __attribute__((range(-1, 0)))' -D fract='int __attribute__((range(-1, 0)))' -D sat= [源文件]

2. 后续在验证时，可通过ACSL断言来模拟sat的饱和行为，比如对赋值操作添加范围检查。

3. 借助XC32预处理输出 #

在MPLAB中配置XC32编译器，添加预处理参数生成适配Frama-C的中间文件：

1. 在XC32编译选项中添加-D _Fract=int -D fract=int -D sat=
2. 导出预处理后的.i文件
3. 直接用Frama-C分析这个.i文件，跳过自身预处理步骤

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