--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on May 2011 ---
Hello, running ???????? frama-c? -jessie? -jessie-atp? coq? t.c?? I get the follwing? error. [kernel] preprocessing with "gcc -C -E -I.? -dD t.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir t.jessie [jessie] File t.jessie/t.jc written. [jessie] File t.jessie/t.cloc written. [jessie] Calling Jessie tool in subdir t.jessie Generating Why function foo [jessie] Calling VCs generator. why -coq [...] why/t.why coqc -I coq coq/t_why.v File "/local/local_git/t.jessie/coq/t_why.v", line 4, characters 8-25: Error: The reference frame_between_sub was not found in the current environment. seems to be a misconfiguration in how frama-c manages why and coqc. Does it look familiar? This is what I have:? the system is a current debian stable i.e. 6.0 ?The coqc is the system's default. The frama-c and why packages are freshly downloaded from their sites. $ why --version This is why version 2.29, compiled on ??? ??? 24 17:08:36 MSD 2011 Copyright (c) 2002 Jean-Christophe Filli?tre This is free software with ABSOLUTELY NO WARRANTY (use option -warranty) $ frama-c --version Version: Carbon-20110201 Compilation date: Tue May 24 16:55:13 MSD 2011 Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable) Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable) Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable) $ coqc --version The Coq Proof Assistant, version 8.2pl2 (July 2010) compiled on Jul 02 2010 15:47:55 with OCaml 3.11.2 ? thanks, Alexander -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110524/921bf10b/attachment.htm>