CODEWITHSUNDEEP
why3
Ben Hocking
Ben Hocking

Reputation: 8092

Need help defining a machine integer

I'm using the mach.int library in a specification (see also this question), and I'm trying to define a constant that is of type int32:

let constant_out1: int32 = 1 in
…

However, when analyzing this, why3 returns the message:

This term has type int, but is expected to have type int32

I noticed that Bounded_int (which Int32 instantiates with type int32) has the following in it:

  val of_int (n:int) : t
    requires { "expl:integer overflow" in_bounds n }
    ensures  { to_int result = n }

However, I do not seem to be able to use this to cast 1 to int32. For example, if I use:

let constant_out1: int32 = Int32.of_int(1) in
…

I get the message unbound symbol 'Int32.of_int'. I've tried many permutations of this, all without any success. Can anyone provided guidance for how to tell why3 that I want 1 to be of type int32?

Upvotes: 3

Views: 138

Answers (0)

Related Questions