Merge branch '694-wp-why-3-output-of-types-with-constructors' into 'master'

Resolve "[wp] why-3 output of types with constructors"

Closes #694

See merge request frama-c/frama-c!2413

src/plugins/qed/export_coq.ml

@@ -320,7 +320,7 @@ struct
                 (fun (c,ts) ->
                    fprintf fmt "@ | @[<hov 2>%s : " (link_name (self#link c)) ;
                    List.iter (fun t -> fprintf fmt "@ %a ->" self#pp_tau t) ts ;
-                   fprintf fmt "@ %a.@]" self#pp_tau result ;
+                   fprintf fmt "@ %a@]" self#pp_tau result ;
                 ) cases ;
               fprintf fmt ".@]@\n" ;
             end

src/plugins/wp/tests/wp_bts/bts_2471.i

+/* run.config
+   DONTRUN:
+ */
+
+/* run.config_qualif
+   OPT: -wp-timeout 1
+   OPT: -wp-prover native:alt-ergo -wp-timeout 1
+   OPT: -wp-prover native:coq
+ */
+
+/*@ axiomatic maps {
+      type model_digit = octet | sextet;
+      logic integer foo(model_digit i);
+    }
+*/
+
+int foo()
+{
+  // Shall not fail (parse error in BTS issue)
+  //@assert ko: \forall int i; i == foo(octet);
+  return 0;
+}

src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle

+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Failed] Goal typed_foo_assert_ko
+[wp] Proved goals:    0 / 1
+[wp] Report in:  'tests/wp_bts/oracle_qualif/bts_2471.0.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.0.report.json'
+-------------------------------------------------------------
+Functions           WP     Alt-Ergo        Total   Success
+foo                 -      -                 1       0.0%
+-------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle

+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo (Native)] Goal typed_foo_assert_ko : Unsuccess
+[wp] Proved goals:    0 / 1
+  Alt-Ergo:        0  (unsuccess: 1)
+[wp] Report in:  'tests/wp_bts/oracle_qualif/bts_2471.1.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.1.report.json'
+-------------------------------------------------------------
+Functions           WP     Alt-Ergo        Total   Success
+foo                 -      -                 1       0.0%
+-------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Coq] Goal typed_foo_assert_ko : Default tactic
+[wp] [Coq (Native)] Goal typed_foo_assert_ko : Unsuccess
+[wp] Proved goals:    0 / 1
+  Coq:             0  (unsuccess: 1)
+[wp] Report in:  'tests/wp_bts/oracle_qualif/bts_2471.2.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.2.report.json'
+-------------------------------------------------------------
+Functions           WP     Alt-Ergo        Total   Success
+foo                 -      -                 1       0.0%
+-------------------------------------------------------------