Frama-C中的非确定值整数模型

Question

请告诉我，这是否是Frama中整数和无符号整数的非确定性值的正确模型？

​

/* Suppose Frama-C is installed in /usr/local -default prefix */
#include "/usr/local/share/frama-c/builtin.h"
#include "/usr/local/share/frama-c/libc/limits.h"

...
#define nondet_int() Frama_C_interval(INT_MIN, INT_MAX)
#define nondet_uint() Frama_C_interval(0, UINT_MAX)
...

​

如果我在选项-machdep中使用具有不同体系结构的上述代码，是否有例外？

Answer 1

Frama_C_interval(0, UINT_MAX)可能无法按预期工作的原因之一是Frama_C_interval具有int (int, int)类型。当您碰巧想要整个范围的unsigned int值时，这实际上会有所帮助，因为引入的转换受近似限制，但通常情况下，Frama_C_interval被声明为返回int这一事实是很麻烦的。

最新发布的版本已经有了Frama_C_unsigned_int_interval，但它是在share/libc/__fc_builtin.h中(安装在/usr/local/share/frama-c/libc/__fc_builtin.h上)。builtin.h文件看起来像是残留下来的遗迹，特别是$Id$行可以追溯到在SVN下完成开发时。

为了指定一个值应该是所有可能的unsigned int值，Frama_C_unsigned_int_interval(0, -1)为自己省去了包含limit.h的麻烦。作为参数传递的int值-1按照C规则转换为最大的unsigned int。

Answer 2

不，在Neon版本中，如果要使用另一个-machdep，则必须手动定义适当的宏。您通常会得到这样的命令行：

frama-c -cpp-extra-args="-D__FC_MACHDEP_X86_64" -machdep x86_64

即将发布的钠将使-cpp-extra-args变得不必要，并且默认提供一个-I选项，让预处理程序搜索Frama的libc头，这样您就不必自己提供它，或者在#include指令中依赖绝对路径。

注：这个答案不是对钠释放的任何特定日期的承诺。