2021-03-02 02:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002218Frama-CKernel > ACSL implementationpublic2016-06-21 14:08
Assigned Tovirgile 
PlatformOSUbuntuOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002218: Specification for sigsetjmp is invalid
DescriptionThe following is code from setjmp.h

typedef int jmp_buf[5]; // arbitrary size
typedef struct {jmp_buf buf; sigset_t sigs;} sigjmp_buf;

/*@ assigns env.buf[0..4]; // unsound - should "assigns \anything" */
int sigsetjmp(sigjmp_buf env, int savesigs);

The assignment clause is not valid, as it references a formal parameter.
This file is incorrectly accepted by frama-c because of the kernel bug in issue 0002217. However, any usage of the function in wp results in the error: [wp] user error: Address of logic value (tmp_0)
TagsNo tags attached.
Attached Files




yakobowski (manager)

Indeed. We found this bug independently, and removed the faulty specification (which was arbitrary on top of being wrong). The fix will be present in Aluminium. Thanks for your report.

-Issue History
Date Modified Username Field Change
2016-03-17 21:15 Ian New Issue
2016-03-17 21:15 Ian Status new => assigned
2016-03-17 21:15 Ian Assigned To => virgile
2016-03-22 22:15 yakobowski Note Added: 0006171
2016-03-22 22:15 yakobowski Status assigned => resolved
2016-03-22 22:15 yakobowski Fixed in Version => Frama-C Aluminium
2016-03-22 22:15 yakobowski Resolution open => fixed
2016-06-21 14:08 signoles Status resolved => closed
+Issue History