0001818: Global variables are not marked as initialized

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001818

Frama-C

Plug-in > E-ACSL

public

2014-06-25 09:58

2014-09-15 17:20

Reporter

arvidj

Assigned To

signoles

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001818: Global variables are not marked as initialized

Description

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;
  }

Tags

No tags attached.

Attached Files

Relationships

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

Issue History
Date Modified	Username	Field	Change
2014-06-25 09:58	arvidj	New Issue
2014-06-25 09:58	arvidj	Status	new => assigned
2014-06-25 09:58	arvidj	Assigned To	=> signoles
2014-06-26 15:13	signoles	Status	assigned => confirmed
2014-08-05 13:59	signoles	Status	confirmed => resolved
2014-08-05 13:59	signoles	Resolution	open => fixed
2014-09-15 17:20	signoles	Fixed in Version	=> Frama-C Neon-20140301
2014-09-15 17:20	signoles	Note Added: 0005458
2014-09-15 17:20	signoles	Status	resolved => closed