Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002395Frama-CPlug-in > clangpublic2018-08-24 00:002018-09-07 08:36
Reporterabhishek.anand.iitg@gmail.com 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSManjaroOS Version8/23/2018
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002395: const fields in constructors
DescriptionConst fields in constructors are not handled properly.

Below is an example:

class A {
public:
  const int x;
  A(int y): x(y){}
};

int main()
{
  A a(0);
}


I get the following error:
root@27db7a69b96a:/hostshare# frama-c -print constFieldBug.cpp
[kernel] Parsing constFieldBug.cpp (external front-end)
Now output intermediate result
[kernel] constFieldBug.cpp:4: User Error:
  Cannot assign to non-modifiable lval this->x
[kernel] User Error: stopping on file "constFieldBug.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.



Perhaps such constructors have to first initialize all fields using the {} notation and then do the rest of the construction of all fields and then do the rest of the constructor body.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006636)
abhishek.anand.iitg@gmail.com (reporter)
2018-08-24 00:02

Here is a smaller example to reproduce the error.

class A {
public:
  const int x;
  A(int y): x(y){}
};
(0006642)
virgile (developer)
2018-09-07 08:36

In the general case, making the initialization explicit at C level would be tricky, as it can involve arbitrary computation (especially if the const field is itself an object upon which a constructor is supposed to be called). The next Frama-C version will be equipped with some mechanism allowing to bypass const checking for write access when in a constructor or when the target is mutable, and Frama-Clang will take advantage of that.

- Issue History
Date Modified Username Field Change
2018-08-24 00:00 abhishek.anand.iitg@gmail.com New Issue
2018-08-24 00:00 abhishek.anand.iitg@gmail.com Status new => assigned
2018-08-24 00:00 abhishek.anand.iitg@gmail.com Assigned To => virgile
2018-08-24 00:02 abhishek.anand.iitg@gmail.com Note Added: 0006636
2018-09-07 08:36 virgile Note Added: 0006642


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker