Unused variable
On this small program
module Global_logic_declarations
use mach.int.Int32
use ref.Ref
type s = {
a_from_struct_S : Int32.int32
}
let rec f () : Int32.int32
ensures { result = 12 }
=
let x = (Ref.ref (any s) : Ref.ref s) in
Ref.(:=) x { (Ref.(!) x) with a_from_struct_S = 12 };
(Ref.(!) x).a_from_struct_S
end
Why3 tells me
warning: unused variable q
Ref.(:=) x { (Ref.(!) x) with a_from_struct_S = 12 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
But, there is no variable q
at all declared in my program, nor in mach.int.Int32
or Ref.ref
. Does this warning warn a real problem or can it be removed?