0002135: sigsetjmp and siglongjmp in setjmp.h

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Tags

No tags attached.

Attached Files

frama-c-sigsetjmp.patch [^] (755 bytes) 2015-06-25 19:37 [Show Content] [Hide Content]

diff -ur frama-c-Sodium-20150201.orig/share/libc/setjmp.h frama-c-Sodium-20150201/share/libc/setjmp.h
--- frama-c-Sodium-20150201.orig/share/libc/setjmp.h	2015-06-23 16:06:03.000000000 -0400
+++ frama-c-Sodium-20150201/share/libc/setjmp.h	2015-06-25 13:23:28.000000000 -0400
@@ -23,15 +23,28 @@
 #ifndef __FC_SETJMP
 #define __FC_SETJMP
 typedef char jmp_buf[5];
+typedef char sigjmp_buf[6];
 
 /*@ 
   assigns env[0..5];
 */
 int setjmp(jmp_buf env);
 
+/*@ 
+  assigns env[0..6];
+*/
+int sigsetjmp(sigjmp_buf env, int savemask);
+
 /*@
  terminates \false; // Unsupported anyway...
  assigns \nothing ;
 */
 void longjmp(jmp_buf env, int val);
+
+/*@ 
+  terminates \false;
+  assigns \nothing;
+*/
+void siglongjmp(sigjmp_buf env, int val);
+
 #endif

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