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 ]
IDProjectCategoryView StatusLast Update
0002135Frama-CKernel > libcpublic2017-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)

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)

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