Jessie: the 'R' reference seems to be not present in the current release (Real for coq ?)
ID0000027: This issue was created automatically from Mantis Issue 27. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000027 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-12-03 |
| Reporter | virgile | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Lithium-20081201 | Target Version | - | Fixed in Version | - |
Description :
[bug 7104 of old BTS, reported by Nicolas Stouls] when calling
cd t.jessie
make -f t.makefile coq-goals after a "frama-c t.c -jessie-anaysis -jessie-gui" The following error is returned :
coqc -I coq coq/t_ctx_why.v Error while reading (...)/t.jessie/coq/t_ctx_why.v : File "(...)/t.jessie/coq/t_ctx_why.v", line 139, characters 46-47 Error: The reference R was not found in the current environment make: *** [coq/t_ctx_why.vo] Erreur 1
Currently, the context file generated by Jessie (t_ctx_why.v) includes some Defintions such as :
(Why logic) Definition add_real : R -> R -> R. Admitted.
but R is not defined.
Regards, Nicolas.
Additional Information :
Depends upon coq 8.2?