[Why3-club] why3 execute: Cannot execute expression match

David MENTRE dmentre at linux-france.org
Fri Aug 19 17:45:42 CEST 2016

Hello Guillaume,

Le 19/08/2016 à 14:48, Guillaume Melquiond a écrit :
> Don't bother, it should be easy enough to fix (assuming my
> interpretation is correct).
[ ~20 minutes later: ]
> And the patch is now on the bugfix/v0.87 branch.


>> > Is there a work-around?
> In the meantime, using your own boolean type rather than the standard
> one should do the trick.

I failed to do it despite several attempts, see attached execute_test.mlw:
$ why3 -C why3.config execute execute_test.mlw Execute_test.test
Execution of Execute_test.test ():
     type: bool

Execution error: Cannot execute expression
                 match ((b1,
                 b2)) with
                 | DFalse, DTrue -> (DTrue)
                 | _, _ -> (DFalse)

It is also apparently not possible to overwrite default 'bool' type.

For now, I removed the match constructions in my code. Much less
readable but it works. :-( Fortunately, thanks to Why3, I found a bug in
the rewritten code because all my properties where not replayed. :-)

I also tried OCaml code generation as another workaround. It works but
it is much more cumbersome to use.

Regarding the output of execute, it would be nicer if records could be
printed with their source code format.

I.e., instead of:
     type: (output_t, internal_state_t)
  ((mk_output_t true false false true true),
  (mk_internal_state_t false false (mk_counter_t 1 1 false)))
  ({ x1 = true; x2 = false; x3 = false; x4 = true; x5 = true }, [...])

It would be more readable.

Another nice feature would be a step-by-step execution of the WhyML
code, to see intermediate computations in the program, like in a debugger.

Last step would be to combine counter-example generation and execution,
the produced counter-example being fed to 'why3 execute'. I know I know,
Why3 is open-source and I should just provide a patch. :-)

Thank you for the quick feedback!
Best regards,

-------------- next part --------------
module Execute_test

 type bool_t = DTrue | DFalse (* work-around for execute bug in Why3 0.87.0 *)

 function bool_t_of_bool (b : bool) : bool_t
 = match b with True -> DTrue | False -> DFalse end

 function bool_of_bool_t (b : bool_t) : bool
 = match b with DTrue -> True | DFalse -> False end

 let f (cmd_previous cmd_current : bool) : bool
 = let b1, b2 = (bool_t_of_bool cmd_previous, bool_t_of_bool cmd_current) in
   let r = match b1, b2 with
   | DFalse, DTrue -> DTrue
   | _, _ -> DFalse
   end in
   bool_of_bool_t r

 let test ()
 = f False True


More information about the Why3-club mailing list