[patch] teach Array.append to Pinterp
I'm going through the why3 tutorial in the manual, now at the MaxAndSum problem ( http://why3.lri.fr/doc/whyml.html#sec17 ). The manual does not give an example of how to actually test the program! I wrote some test code
let test () = let one x = Array.make 1 x in let (++) a b = Array.append a b in max_sum (one 1 ++ one 3 ++ one 2)
and I found some documentation in how to actually run the test in section 7.1 ( http://why3.lri.fr/doc/exec.html#sec101 ). But running my test code (which is different from the one in 7.1) exhibits the following behavior:
File "../buffer/max_and_sum.mlw", line 3, characters 2-20: warning: the keyword `import' is redundant here and can be omitted File "../buffer/max_and_sum.mlw", line 4, characters 2-20: warning: the keyword `import' is redundant here and can be omitted File "../buffer/max_and_sum.mlw", line 5, characters 2-24: warning: the keyword `import' is redundant here and can be omitted Execution of MaxAndSum.test (): type: (int, int) anomaly: Why3.Pinterp.CannotCompute
After scratching my head, I figured out that the problem is with the Array.append function, which is defined as a built-in in the standard library. The following patch (suitable for
git am application)
lets pinterp.ml know about Array.append, and now my code above successfully computes the expected result.
There is also a
mlinterp.ml file which looks very similar and also lacks an
Array.append primitive. What is this file used for? Should I also add the primitive there?