View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002135 | Frama-C | Kernel > libc | public | 2015-06-25 19:37 | 2017-05-23 13:42 | ||||
Reporter | mansour | ||||||||
Assigned To | maroneze | ||||||||
Priority | normal | Severity | feature | Reproducibility | N/A | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Sodium | ||||||||
Target Version | Fixed in Version | Frama-C Aluminium | |||||||
Summary | 0002135: sigsetjmp and siglongjmp in setjmp.h | ||||||||
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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
maroneze (administrator) 2015-07-17 17:44 |
Thank you for reporting it. A modified specification has been added, for completion, although these functions are currently unsupported by Frama-C. This has been clarified in the file, and will be available either in the next release of Frama-C, or the one following that. As a side note, the use of "terminates \false" has been replaced with "ensures \false", which better reflects the semantics of longjmp/siglongjmp. |
maroneze (administrator) 2017-05-23 13:42 |
Prototypes added (to allow parsing to succeed), but as stated, these functions are unsupported by most plug-ins. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-06-25 19:37 | mansour | New Issue | |
2015-06-25 19:37 | mansour | Status | new => assigned |
2015-06-25 19:37 | mansour | Assigned To | => virgile |
2015-06-25 19:37 | mansour | File Added: frama-c-sigsetjmp.patch | |
2015-07-17 08:36 | signoles | Assigned To | virgile => maroneze |
2015-07-17 08:36 | signoles | Category | Kernel > ACSL implementation => Kernel > libc |
2015-07-17 17:44 | maroneze | Note Added: 0005987 | |
2017-05-23 13:42 | maroneze | Note Added: 0006398 | |
2017-05-23 13:42 | maroneze | Status | assigned => resolved |
2017-05-23 13:42 | maroneze | Fixed in Version | => Frama-C Aluminium |
2017-05-23 13:42 | maroneze | Resolution | open => fixed |
2017-05-23 13:42 | maroneze | Status | resolved => closed |