Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002217Frama-CKernelpublic2016-03-17 21:132016-06-21 14:08
ReporterIan 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSUbuntuOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002217: Frama-c accepts assigning formal parameters when a range is used
DescriptionWhen assigning a range, no error is produced when referencing a formal parameter.
Steps To Reproducetest.c: typedef struct obj { char buf[5]; } obj; /*@ assigns x.buf[0..0]; */ void foo(obj x); void bar() { obj tmp; foo(tmp); //@ assert \true; } Running as given above produces no error (it should). > frama-c test.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing test.c (with preprocessing) Running the above program with wp causes an error. > frama-c test.c -wp [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing test.c (with preprocessing) [wp] warning: Missing RTE guards test.c:6:[wp] user error: Address of logic value (tmp_0) [kernel] Plug-in wp aborted: invalid user input. Changing the specification of foo to “assigns x.buf[0]” results in the expected error. > frama-c test.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing test.c (with preprocessing) test.c:6:[kernel] user error: can not assign part of a formal parameter: x.buf[0] [kernel] user error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006173)
yakobowski (manager)
2016-03-22 22:17

We have tightened the checks for non-assignable terms, and your programs is now rejected as expected. Thanks for the report.

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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker