小编cod*_*ody的帖子

我对 Frama-C 18.0 版（Argon）的行为有些困惑。

鉴于以下程序：

#include <assert.h>
#include <limits.h>


/*@ requires order: min <= max;
    assigns \result \from min, max;
    ensures result_bounded: min <= \result <= max ;
 */
extern int Frama_C_interval(int min, int max);


int main() {

  int i,j;

  i = Frama_C_interval(INT_MIN, INT_MAX);

  j = i;

  assert(j == i);

  return 0;
}

我希望可以很容易地用任何跟踪平等的抽象域来证明这个断言。但是，调用

框架-c -eva -eva-equality-domain -eva-polka-equalities foo.c

给出：

[eva] Warning: The Apron domains binding is experimental.
[kernel] Parsing stupid_test.c (with preprocessing)
[eva] Analyzing a complete application starting at …

我正在使用 Z3 源目录中的以下（标准）命令从源代码中使用 OCaml 编译 Z3：

> python scripts/mk_make.py --prefix=$OPAM_SWITCH_PREFIX --ml

然后从build/目录中构建和安装。

然后运行

> utop

和

> #require "z3";;

给了我以下错误：

Cannot load required shared library dllz3ml. Reason: /home/foobar/.opam/my_opam/lib/stublibs/dllz3ml.so: undefined symbol: Z3_rcf_del.

我对如何调试这些类型的错误感到困惑。是否有任何建议可以确定问题以及如何解决？