--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to use ACSL in GUI and How to generateCoqcode



On Wed, Dec 2, 2009 at 3:40 PM, CUOQ Pascal <Pascal.CUOQ at cea.fr> wrote:
>
>> http://frama-c.cea.fr/download/frama-c-Beryllium-20090902-why-2.21.tar.gz.
>> But I got a syntax error at line 604, file src/kernel/db.ml
>
>> (** Detection of the unused code of an application. *)
>> module Sparecode = struct
>> ?let get =
>> ? ?ref (fun ~select_annot:_ ?-> not_yet_implemented "Sparecode.run")
>> ?let rm_unused_globals =
>> ? ?ref (fun ?project:_ -> not_yet_implemented
>>"Sparecode.rm_unused_glob") ? (*this is line 604*)
>>end
>
>> I tried both
>>ocaml 3.10.2 and the latest
>>3.11.1, got the same errors.
>
> This is very strange, as the archive that you mention has been compiled
> countless times without problem with both OCaml versions.
> Are you positive that you are using 3.10.2 or 3.11.1 each time?
> Did you, by any chance, compile only ocamlc and ocamlopt when
> you were installing OCaml, leaving ocamlc.opt and ocamlopt.opt
> provided by an older package in your distribution?
>
> Try:
> ocamlc -v
> ocamlopt -v
> ocamlc.opt -v
> ocamlopt.opt -v
>
> Also try de-installing any old OCaml package from your distribution,
> if package dependencies do not make it too annoying.

Thanks. It works after I uninstalled other older OCaml, and reinstalled again.

>
> Pascal
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>