Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002135Frama-CKernel > libcpublic2015-06-25 19:372017-05-23 13:42
Reportermansour 
Assigned Tomaroneze 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002135: sigsetjmp and siglongjmp in setjmp.h
DescriptionHello,

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.
TagsNo tags attached.
Attached Filespatch file icon frama-c-sigsetjmp.patch [^] (755 bytes) 2015-06-25 19:37 [Show Content]

- Relationships

-  Notes
(0005987)
maroneze (developer)
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.
(0006398)
maroneze (developer)
2017-05-23 13:42

Prototypes added (to allow parsing to succeed), but as stated, these functions are unsupported by most plug-ins.

- Issue History
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker