--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] coqc: The reference frame_between_sub was not found in the current environment



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>