Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why3-club] why3-0.88.0 and CVC4 1.4/1.5

it is

why3 prove -P CVC4,1.5 ...

sorry for the confusion between -P and -D

- Claude


Le 24/10/2017 à 16:10, Gerlach, Jens a écrit :
> Hello Claude, 
> 
> I tried your suggestion on one of our examples 
> 	why3 prove -D CVC4,1.5 find_assert_rte_mem_access_Alt-Ergo.mlw
> and received the following error message
> 	anomaly: Sys_error("CVC4,1.5: No such file or directory")
> 
> When I try
> 	why3 prove -D CVC4 find_assert_rte_mem_access_Alt-Ergo.mlw
> the error message is a bit more specific
> 	anomaly: Sys_error("/home/jens/.opam/system/share/why3/drivers/CVC4.drv: No such file or directory")
> 
> In  ~/.opam/system/share/why3/drivers/ there are
> 
> 	cvc4_14.drv
> 	cvc4_15.drv
> 	cvc4_bv.gen
> 	cvc4.drv
> 	cvc4-realize.drv
> 
> Regards
> 
> Jens
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> 

-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - ÃŽle-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |