frama-c - 在 Frama-C 中对非确定性值整数进行建模

Question

有人可以告诉我这是 Frama-C 中整数和无符号整数的非确定性值的正确模型吗？

/* 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 中使用具有不同架构的上述代码，是否有任何异常(exception)？

Answer 1

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

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

即将发布的 Sodium 将使 -cpp-extra-args 不再需要，并且默认提供 -I 选项，让预处理器搜索 Frama-C 的 libc header ，这样您就不必自己提供它或依赖 #include 指令中的绝对路径

注意:此答案并非对 Sodium 发布的任何特定日期的 promise 。