mach.int库是why3的默认部分吗？

Question

我试图在Simulink模型的Why3规范中使用32位整数，并且我找到了mach.int库，至少在一个地方，被描述为标准库的一部分。但是，当我尝试将其用于以下导入命令时：

  use import mach.int.Int32

我收到这样的信息：

Library file not found: mach.int

这是我第一个用“。”在它中，我不确定我的语法是否错误，或者这个库实际上不是标准库的一部分，或者我是否做了其他错误。

使用mach.int.Int32模块的正确方法是什么？

附加细节

我的why3版本是0.87.3：

▶ why3 --version
Why3 platform, version 0.87.3

我查看了我的~/.why3.conf文件，发现了以下几行：

[main]
loadpath = "/opt/gps/share/why3/theories"
loadpath = "/opt/gps/share/why3/modules"
loadpath = "/opt/gps/share/spark/theories"

我查看了/opt/gps/share/why3/modules (以及/opt/gps/share/why3/theories和/opt/gps/share/spark/theories)，没有找到mach.int.*，所以我在/opt/gps/share/why3/modules中创建了一个mach.int.mlw文件，并确保why3对此没有意见：

▶ why3 prove -P z3 mach.int.mlw        
mach.int.mlw Int WP_parameter infix / : Valid (0.01s)
mach.int.mlw Int WP_parameter infix % : Valid (0.01s)
mach.int.mlw Refint63 WP_parameter incr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter decr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix += : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix -= : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix *= : Valid (0.02s)
mach.int.mlw MinMax63 WP_parameter min : Valid (0.01s)
mach.int.mlw MinMax63 WP_parameter max : Valid (0.02s)

结果是一样的。

Answer 1

原来，why3是在mach子目录中的模块int.mlw中寻找mach。

将图书馆放在/opt/gps/share/why3/modules/mach/目录中可以解决找不到库的问题(在这个库中，/opt/gps/share/why3/modules被定义为/opt/gps/share/why3/modules/mach/文件中的loadpath的一部分)。