I'm trying to use 32-bit integers in a Why3 specification of a Simulink model, and I've found the mach.int library, that is, at least in one place, described as being part of the standard library. However, when I try to use it with the following importing command:
use import mach.int.Int32
I get the message:
Library file not found: mach.int
This is my first library with a "." in it, so I'm not sure if my syntax is wrong, or this library isn't actually part of the standard library, or if I'm doing something else wrong.
What is the proper way to use the mach.int.Int32 module?
My why3 version is 0.87.3:
▶ why3 --version
Why3 platform, version 0.87.3
I looked in my ~/.why3.conf file and found these lines:
[main]
loadpath = "/opt/gps/share/why3/theories"
loadpath = "/opt/gps/share/why3/modules"
loadpath = "/opt/gps/share/spark/theories"
I looked in /opt/gps/share/why3/modules (and /opt/gps/share/why3/theories and /opt/gps/share/spark/theories) and found no mach.int.*, so I created a mach.int.mlw file in /opt/gps/share/why3/modules, and made sure that why3 was OK with it:
▶ 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)
The result is the same.
It turns out that why3 was looking for mach.int.Int32 in a module int.mlw in a mach subdirectory.
Putting the mach.int library in the /opt/gps/share/why3/modules/mach/ directory solves the problem with the library not being found (where /opt/gps/share/why3/modules is defined as part of loadpath in my ~/.why3.conf file).