Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:50 CET
  

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 
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 Files
  • patch file icon frama-c-sigsetjmp.patch (755 bytes) 2015-06-25 19:37 - 
    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
    patch file icon frama-c-sigsetjmp.patch (755 bytes) 2015-06-25 19:37 +

-Relationships
+Relationships

-Notes

~0005987

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.

~0006398

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.
+Notes

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