Frama-C Bug Tracking System - Frama-C
View Issue Details
0000759Frama-CPlug-in > Evapublic2011-03-21 17:182014-02-12 16:59
ddelmas 
pascal 
normalmajoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Oxygen-20120901Frama-C Oxygen-20120901 
0000759: wrong treatment for const arrays in lib-entry mode
With the attache source file,
frama-c fptr.c -lib-entry -main f -users

yields the below incorrect result:
[users] ====== DISPLAYING USERS ======
        f: h0 h1
        ====== END OF USERS ==========
No tags attached.
related to 0001026closed yakobowski value analysis memory consumption problem when using -lib-entry option 
c fptr.c (322) 2011-03-21 17:18
https://bts.frama-c.com/file_download.php?file_id=185&type=bug
Issue History
2011-03-21 17:18ddelmasNew Issue
2011-03-21 17:18ddelmasStatusnew => assigned
2011-03-21 17:18ddelmasAssigned To => pascal
2011-03-21 17:18ddelmasFile Added: fptr.c
2011-03-21 20:57pascalCategoryPlug-in > users => Plug-in > value analysis
2011-03-21 20:57pascalSummarywrong set of calls in lib-entry mode => wrong treatment for const arrays in lib-entry mode
2011-03-21 20:58pascalNote Added: 0001621
2011-03-21 21:15pascalNote Added: 0001622
2011-03-21 21:26pascalNote Deleted: 0001622
2011-03-21 21:30pascalNote Added: 0001623
2011-03-21 21:47pascalNote Edited: 0001623
2011-03-21 21:48svnCheckin
2011-03-21 21:48svnStatusassigned => resolved
2011-03-21 21:48svnResolutionopen => fixed
2011-03-22 11:28pascalNote Added: 0001626
2011-03-22 11:28pascalStatusresolved => feedback
2011-03-22 11:28pascalResolutionfixed => reopened
2011-03-22 11:28pascalStatusfeedback => confirmed
2011-05-13 22:05pascalNote Added: 0001893
2012-04-07 23:56yakobowskiStatusconfirmed => assigned
2012-04-07 23:56yakobowskiAssigned Topascal => yakobowski
2012-04-07 23:57yakobowskiRelationship addedrelated to 0001026
2012-04-08 00:06yakobowskiTarget Version => Frama-C Oxygen-2012xx01
2012-04-11 10:26yakobowskiNote Added: 0002857
2012-05-19 17:01svnCheckin
2012-05-19 17:01svnStatusassigned => resolved
2012-05-19 17:01svnResolutionreopened => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:59pascalNote Added: 0004822
2014-02-12 16:59pascalAssigned Toyakobowski => pascal
2014-02-12 16:59pascalStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0001621)
pascal   
2011-03-21 20:58   
Note that the bug is not specific to option -users or function pointers. It can be produced with:


const int t[] = { 1, 2, 3, 4, 5 } ;

main()
{
  Frama_C_dump_each();
}

$ frama-c -lib-entry t.c -val

[value] Values of globals at initialization
        t[0] ? {1; }
         [1] ? {2; }
         [2..4] ? {1; 2; }
(0001623)
pascal   
2011-03-21 21:30   
(edited on: 2011-03-21 21:47)
Workaround: write "int (const t)[] = { 1, 2, 3, 4, 5 } ;" instead, or apply:

Index: src/value/eval.ml
===================================================================
--- src/value/eval.ml (revision 12393)
+++ src/value/eval.ml (working copy)
@@ -2056,14 +2056,19 @@
   let rec add_offsetmap depth v name_desc name typ offset_orig typ_orig state =
     let typ = Cil.unrollType typ in
     let loc = loc_of_typoffset v typ_orig offset_orig in
+ let rec treat_as_const typ =
+ (hasAttribute "const" (typeAttrs typ)) ||
+ ( match typ with
+ TArray (typ, _,_,_) -> treat_as_const (Cil.unrollType typ)
+ | _ -> false)
+ in
     let must_initialize =
       initializing_formal ||
- (not (hasAttribute "const" (typeAttrs typ))) ||
- (Cvalue_type.V.equal
+ (not (treat_as_const typ)) ||
+ (Cvalue_type.V.is_bottom
             (Relations_type.Model.find
         ~conflate_bottom:true ~with_alarms:CilE.warn_none_mode
- state loc)
- Cvalue_type.V.bottom)
+ state loc))
     in
     if not must_initialize
       (* if we do not have an initializer for this const, we generate

(0001626)
pascal   
2011-03-22 11:28   
The bug is not completely fixed by the patch. It would still be visible with arrays of structs, the struct having some const fields. The underlying algorithm needs to be revised in order to fix this completely.
(0001893)
pascal   
2011-05-13 22:05   
And someone complained about a performance regression with the patch above so that it was changed into yet something else in the development version. This is too much work to bother back-porting to 20110201 now.
(0002857)
yakobowski   
2012-04-11 10:26   
Up-to-date example where the const qualifier is not honored.

typedef struct {
  int f1;
  const int f2;
} s;

s t1[] = {1, 2, 3, 4, 5, 6, 7, 8};

void main() {

}
(0004822)
pascal   
2014-02-12 16:59   
Fix committed to stable/neon branch.