Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002218Frama-CKernel > ACSL implementationpublic2016-03-17 21:152016-06-21 14:08
ReporterIan 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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

- Relationships

-  Notes
(0006171)
yakobowski (manager)
2016-03-22 22:15

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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker