frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-01T21:06:09Z
https://git.frama-c.com/pub/frama-c/-/issues/314
File frama-c/libc/features.h should include definition of the macro __GNUC_PR...
2021-04-01T21:06:09Z
Jochen Burghardt
File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
ID0002253:
**This issue was created automatically from Mantis Issue 2253. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002253:
**This issue was created automatically from Mantis Issue 2253. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002253 | Frama-C | Kernel > libc | public | 2016-10-17 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
The macro __GNUC_PREREQ is used in many system include files. It is defined in referring to "/usr/include/features.h"l.
However, a "#include <features.h>" directive is redirected by Frama-C to (e.g.) "~/.opam/system/share/frama-c/libc/features.h" which doesn't define the macro.
Adding the definition there wouldn't cause any harm (? - at least, I can't think of any) and would help to make more system include files work with Frama-C.
https://git.frama-c.com/pub/frama-c/-/issues/538
Specification of the read function
2021-02-22T13:39:02Z
mantis-gitlab-migration
Specification of the read function
ID0001939:
**This issue was created automatically from Mantis Issue 1939. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001939:
**This issue was created automatically from Mantis Issue 1939. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001939 | Frama-C | Kernel > libc | public | 2014-10-19 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mansour | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Hi,
I think it would be useful to have a specification of common libc functions included with Frama-C (instead of repeating them in many projects), so I started with one for the read function.
I think it's complete, but I am still new to ACSL, so correct me if I'm wrong.
Please find attached the diff to the Neon version.
Yours,
Mansour
## Attachments
- [frama-c-Neon-20140301-read-spec.patch](/uploads/66ae8ded47ce423fa95cdf4d8587ae04/frama-c-Neon-20140301-read-spec.patch)
https://git.frama-c.com/pub/frama-c/-/issues/536
redefinition of size_t, time_t, FILE
2021-02-22T13:38:40Z
mantis-gitlab-migration
redefinition of size_t, time_t, FILE
ID0002171:
**This issue was created automatically from Mantis Issue 2171. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002171:
**This issue was created automatically from Mantis Issue 2171. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002171 | Frama-C | Kernel > libc | public | 2015-09-29 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Hi,
if I include both <stdio.h> and <builtin.h> to get things like Frama_C_interval() it will give the following errors:
FRAMAC_SHARE/machine.h:67:[kernel] user error: redefinition of 'size_t' in the same scope. Previous declaration was at FRAMAC_SHARE/libc/__fc_define_size_t.h:26
FRAMAC_SHARE/machine.h:70:[kernel] user error: redefinition of 'time_t' in the same scope. Previous declaration was at FRAMAC_SHARE/libc/__fc_define_time_t.h:25
FRAMAC_SHARE/machine.h:88:[kernel] user error: redefinition of 'FILE' in the same scope. Previous declaration was at FRAMAC_SHARE/libc/__fc_define_file.h:39
machine.h has them as typedefs while the other files have them as #defines.
Kurt
https://git.frama-c.com/pub/frama-c/-/issues/349
sigsetjmp and siglongjmp in setjmp.h
2021-02-22T12:59:58Z
mantis-gitlab-migration
sigsetjmp and siglongjmp in setjmp.h
ID0002135:
**This issue was created automatically from Mantis Issue 2135. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002135:
**This issue was created automatically from Mantis Issue 2135. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002135 | Frama-C | Kernel > libc | public | 2015-06-25 | 2017-05-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mansour | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Hello,
This patch adds the function prototypes of sigsetjmp and siglongjmp to the header setjmp.h.
The type definition of sigjmp_buf is like jmp_buf but one character longer.
## Attachments
- [frama-c-sigsetjmp.patch](/uploads/c11c75898be46a528d848476dc1e271b/frama-c-sigsetjmp.patch)
https://git.frama-c.com/pub/frama-c/-/issues/229
FE_* API is available on OpenBSD
2021-02-22T12:56:52Z
mantis-gitlab-migration
FE_* API is available on OpenBSD
ID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002379 | Frama-C | Kernel > libc | public | 2018-06-18 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | any | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
please include attached patch.
## Attachments
- [patch-src_libraries_utils_c_bindings_c](/uploads/5d11f5d41c049aab5269993f94365e40/patch-src_libraries_utils_c_bindings_c)
https://git.frama-c.com/pub/frama-c/-/issues/63
unistd.h declares __fc_ttyname but it has no definition
2021-02-22T12:52:15Z
mantis-gitlab-migration
unistd.h declares __fc_ttyname but it has no definition
ID0002489:
**This issue was created automatically from Mantis Issue 2489. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002489:
**This issue was created automatically from Mantis Issue 2489. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002489 | Frama-C | Kernel > libc | public | 2020-01-08 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vkraus | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | opam | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
When compiling __fc_runtime.c, I get
/usr/bin/ld: __fc_runtime.o:(.data.rel+0x0): undefined reference to `__fc_ttyname'
collect2: error: ld returned 1 exit status
### Additional Information :
gcc version 8.3.0 (debian buster)
frama-c version 20.0 (Calcium)
### Steps To Reproduce :
gcc -I$(frama-c -print-share-path)/libc -nostdinc -D__FC_MACHDEP_X86_64 -o __fc_runtime.o -c $(frama-c -print-share-path)/libc/__fc_runtime.c
(ignore the warnings)
echo "int main () { return 0; }" > main.c
gcc main.c __fc_runtime.o
You should get the error.