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 - 2018 MantisBT Team
Powered by Mantis Bugtracker