Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:30 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001469Frama-CKernelpublic2013-08-21 17:312014-03-13 15:57
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001469: Unsound transformation of ACSL annotations
DescriptionTest 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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0004561

2014-02-12 16:57

 Fix committed to stable/neon branch.
+Notes

-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
2013-09-02 15:58 svn Status assigned => resolved
2013-09-02 15:58 svn Resolution open => fixed
2013-12-19 01:11 Source_changeset_attached => framac master 95cb344a
2014-02-12 16:53 Source_changeset_attached => framac stable/neon 95cb344a
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
+Issue History