Frama-C Bug Tracking System - Frama-C
View Issue Details
0001818Frama-CPlug-in > E-ACSLpublic2014-06-25 09:582014-09-15 17:20
arvidj 
signoles 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Neon-20140301 
0001818: Global variables are not marked as initialized
Frama-C Git: b71d80efb3808c286f1a2f17dbf54bc3909824d0 E-ACSL Git: 19aea9a2202efc99fe3e268551e559358aa95751 Example: int a = 0, b; int main(void) { int *p = &a, *q = &b; /*@assert \initialized(&b) ; */ /*@assert \initialized(q) ; */ /*@assert \initialized(p) ; */ } Both a and b should be marked as initialized in the generated __e_acsl_memory_init, but this is not the case: void __e_acsl_memory_init(void) { __store_block((void *)(& a),sizeof(int)); __store_block((void *)(& b),sizeof(int)); return; }
No tags attached.
Issue History
2014-06-25 09:58arvidjNew Issue
2014-06-25 09:58arvidjStatusnew => assigned
2014-06-25 09:58arvidjAssigned To => signoles
2014-06-26 15:13signolesStatusassigned => confirmed
2014-08-05 13:59signolesStatusconfirmed => resolved
2014-08-05 13:59signolesResolutionopen => fixed
2014-09-15 17:20signolesFixed in Version => Frama-C Neon-20140301
2014-09-15 17:20signolesNote Added: 0005458
2014-09-15 17:20signolesStatusresolved => closed

Notes
(0005458)
signoles   
2014-09-15 17:20   
Fixed in E-ACSL v0.4.1.