GitLab

ID0002485: This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002485	Frama-C	Plug-in > wp	public	2019-11-08	2019-11-08

Reporter	jens	Assigned To	correnson	Resolution	open
Priority	normal	Severity	minor	Reproducibility	have not tried
Platform	Linux	OS	xubuntu	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

When the attached programme is processed with

frama-c -wp -wp-rte -wp-prover native:alt-ergo -wp-out abs.wp abs.c

then the output directory 'abs.wp/typed' contains three files

 abs_ensures_3_Alt-Ergo.mlw
 abs_ensures_3_Alt-Ergo.out
 abs_ensures_3.ergo

When using the command line

frama-c -wp -wp-rte -wp-prover alt-ergo -wp-out abs.wp abs.c

then the output directory 'abs.wp/typed' contains only the generated proof obligation

abs_ensures_3_Why3_Alt_Ergo_2_3_0.why

(similiarly when using another Why3 prover, such as cvc4)

Is there a way to output also the result for Why3 provers?

Attachments

• abs.c