Frama-C Bug Tracking System - Frama-C
View Issue Details
0002395Frama-CPlug-in > clangpublic2018-08-24 00:002018-09-07 08:36 
Frama-C 17-Chlorine 
0002395: const fields in constructors
Const 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.
No tags attached.
Issue History
2018-08-24 00:00abhishek.anand.iitg@gmail.comNew Issue
2018-08-24 00:00abhishek.anand.iitg@gmail.comStatusnew => assigned
2018-08-24 00:00abhishek.anand.iitg@gmail.comAssigned To => virgile
2018-08-24 00:02abhishek.anand.iitg@gmail.comNote Added: 0006636
2018-09-07 08:36virgileNote Added: 0006642

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){} };
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.