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] coqc: The reference frame_between_sub was not found in the current environment

  • Subject: [Frama-c-discuss] coqc: The reference frame_between_sub was not found in the current environment
  • From: horsh at mail.ru (Alexander Gorshenev)
  • Date: Tue, 24 May 2011 17:48:58 +0400
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>