--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on August 2017 ---
It seems that something has been changed. ~/D/why-2.38 â¯â¯â¯ autoconf ~/D/why-2.38 â¯â¯â¯ ./configure checking for ocamlc... ocamlc ocaml version is 4.03.0 ocaml library path is /Users/david/.opam/4.03.0/lib/ocaml checking for ocamlfind... yes checking OS dependent settings... Unix checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocamlopt.opt... ocamlopt.opt checking ocamlc.opt version... ok checking for ocamldep... ocamldep checking for ocamldep.opt... ocamldep.opt checking for ocamllex... ocamllex checking for ocamllex.opt... ocamllex.opt checking for ocamlyacc... ocamlyacc checking for ocamldoc... ocamldoc checking for ocamldoc.opt... ocamldoc.opt ocamlfind found ocamlgraph in /Users/david/.opam/4.03.0/lib/ocamlgraph checking for ocamlweb... true checking for frama-c... /Users/david/.opam/4.03.0/bin/frama-c checking Frama-c version... Silicon-20161101 checking for why3... /Users/david/.opam/4.03.0/bin/why3 checking Why3 version... configure: WARNING: unknown version , hope this works checking for coqc... no configure: WARNING: Cannot find coqc. checking for pvs... no configure: WARNING: Cannot find PVS. configure: creating ./config.status config.status: creating Makefile Summary ----------------------------------------- OCaml version : 4.03.0 OCaml library path : /Users/david/.opam/4.03.0/lib/ocaml OcamlGraph lib : found by ocamlfind Verbose make : no Inference of annotations : no Why3 support : yes Binary : /Users/david/.opam/4.03.0/bin/why3 Version : unknown version , hope this works Frama-C plugin : yes Binary : /Users/david/.opam/4.03.0/bin/frama-c Version : Silicon-20161101 Coq support (via Why3) : no command 'coqc' not found PVS support (via Why3) : no command 'pvs' not found Other provers support : (via Why3) Thanks, Junkil > On Aug 22, 2017, at 5:23 AM, Claude Marché <Claude.Marche at inria.fr> wrote: > > > I see, I guess the 'sed' command used to parse the answer does not work > on Mac, maybe because now there is no newline anymore at the end, > something like that > > So a possible workaround : edit the configure.in file, find the first > occurence of Silicon in it, then replace the line above > > FRAMACVERSION=`$FRAMAC -version | sed -n -e 's|\(Version: > \)\?\(.*\)$|\2|p' ` > > by > > FRAMACVERSION=`$FRAMAC -version` > > then > > autoconf > ./configure > > > If autoconf does not work for you, then you should do the modification > directly in the file 'configure' instead > > - Claude > > > > > Le 22/08/2017 à 11:14, Junkil âDavidâ Park a écrit : >> â¯â¯ frama-c --version >> Silicon-20161101% >> >> Thanks, >> Junkil >> >>> On Aug 22, 2017, at 5:13 AM, Claude Marché <Claude.Marche at inria.fr> wrote: >>> >>> >>> >>> Le 22/08/2017 à 10:53, Junkil âDavidâ Park a écrit : >>>> checking Frama-c version... >>>> configure: WARNING: bad Frama-c version "", you need version Silicon >>> >>> there's a bug here... what is the answer of >>> >>> frama-c --version >>> >>> ? >>> >>> -- >>> 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 | >>> _______________________________________________ >>> Frama-c-discuss mailing list >>> Frama-c-discuss at lists.gforge.inria.fr >>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss >> >> _______________________________________________ >> 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 | > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss