2021-03-01 05:13 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000725Frama-CKernelpublic2011-02-17 08:522014-02-12 16:59
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000725: passing (C && c) as argument to a function that expects int (csmith)
Description$ frama-c -val char_ampamp.c

char_ampamp.c:7:[value] reading left-value x.
        The contents is imprecise.
char_ampamp.c:7:[kernel] warning: accessing uninitialized left-value x: assert(Ook)
char_ampamp.c:7:[kernel] warning: accessing left-value x that contains escaping addresses; assert(Ook)
[value] Called Frama_C_show_each_x({{ ANYTHING }})
TagsNo tags attached.
Attached Files
  • c file icon char_ampamp.c (126 bytes) 2011-02-17 14:46 - 
    char c=1;
int y;

void g(int y, int x)
{
  Frama_C_show_each_x(x);
}

main()
{
  y = 42 && c;
  g(c, 42 && c);
  return 0;
}
    c file icon char_ampamp.c (126 bytes) 2011-02-17 14:46 +

-Relationships
+Relationships

-Notes

~0001512

pascal (reporter)

2011-02-17 14:46

 Uncomment Format.printf "expr arg: %a %a@." in src/value/eval.ml.
For the attached program you will see :

expr arg: (int )c int
expr arg: c != (char)0 char

The second one is wrong.

~0004832

2014-02-12 16:59

 Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-02-17 08:52 pascal New Issue
2011-02-17 08:52 pascal Status new => assigned
2011-02-17 08:52 pascal Assigned To => pascal
2011-02-17 08:52 pascal File Added: char_ampamp.c
2011-02-17 14:44 pascal Assigned To pascal => virgile
2011-02-17 14:45 pascal File Deleted: char_ampamp.c
2011-02-17 14:46 pascal File Added: char_ampamp.c
2011-02-17 14:46 pascal Note Added: 0001512
2011-02-17 18:42 svn
2011-02-17 18:42 svn Status assigned => resolved
2011-02-17 18:42 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2011-10-21 14:38 pascal Status closed => feedback
2011-10-21 14:38 pascal Resolution fixed => reopened
2011-10-21 14:39 pascal Category Plug-in > value analysis => Kernel
2011-10-21 14:39 pascal Status feedback => closed
2011-10-21 14:39 pascal Resolution reopened => fixed
2013-12-19 01:12 Source_changeset_attached => framac master c1f9b428
2014-02-12 16:54 Source_changeset_attached => framac stable/neon c1f9b428
2014-02-12 16:59 Note Added: 0004832
2014-02-12 16:59 Status closed => resolved
+Issue History