0001469: Unsound transformation of ACSL annotations

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001469

Frama-C

Kernel

public

2013-08-21 17:31

2014-03-13 15:57

Reporter

pascal

Assigned To

virgile

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001469: Unsound transformation of ACSL annotations

Description

Test in SVN 23392: tests/misc/logic_ptr_cast.i

Obtained result:

[value] Called Frama_C_show_each({{ &t + {0; 4; 8; 12; 16; 20; 24; 28} }})
...
  /*@
  assert
  ((((((p == (int *)t || p == (int *)(&t[1])) || p == (int *)(&t[2])) ||
      p == (int *)(&t[3]))
     || p == (int *)(&t[4]))
    || p == (int *)(&t[5]))
   || p == (int *)(&t[6]))
  || p == (int *)(&t[7]); */

Expected result:

[value] Called Frama_C_show_each({{ &t + {0; 1; 2; 3; 4; 5; 6; 7} }})

and the same assert as the one written in the program.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0004561) 2014-02-12 16:57	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2013-08-21 17:31	pascal	New Issue
2013-08-21 17:32	pascal	Description Updated
2013-08-21 17:33	pascal	Status	new => assigned
2013-08-21 17:33	pascal	Assigned To	=> virgile
2013-09-02 15:58	svn	Checkin
2013-09-02 15:58	svn	Status	assigned => resolved
2013-09-02 15:58	svn	Resolution	open => fixed
2014-02-12 16:57		Note Added: 0004561
2014-03-13 15:56	signoles	Fixed in Version	=> Frama-C Neon-20140301
2014-03-13 15:57	signoles	Status	resolved => closed