Specification for sigsetjmp is invalid
ID0002218: This issue was created automatically from Mantis Issue 2218. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002218 | Frama-C | Kernel > ACSL implementation | public | 2016-03-17 | 2016-06-21 |
| Reporter | Ian | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | Ubuntu | OS Version | - |
| Product Version | Frama-C Magnesium | Target Version | - | Fixed in Version | Frama-C Aluminium |
Description :
The following is code from setjmp.h
typedef int jmp_buf[5]; // arbitrary size typedef struct {jmp_buf buf; sigset_t sigs;} sigjmp_buf;
/*@ assigns env.buf[0..4]; // unsound - should "assigns \anything" */ int sigsetjmp(sigjmp_buf env, int savesigs);
The assignment clause is not valid, as it references a formal parameter. This file is incorrectly accepted by frama-c because of the kernel bug in issue #2217 (closed). However, any usage of the function in wp results in the error: [wp] user error: Address of logic value (tmp_0)