2021-03-02 03:24 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000759Frama-CPlug-in > Evapublic2014-02-12 16:59
Reporterddelmas 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFrama-C Oxygen-20120901Fixed in VersionFrama-C Oxygen-20120901 
Summary0000759: wrong treatment for const arrays in lib-entry mode
DescriptionWith 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 ==========
TagsNo tags attached.
Attached Files
  • c file icon fptr.c (322 bytes) 2011-03-21 17:18 -
    //@ assigns \nothing;
    extern void h0();
    //@ assigns \nothing;
    extern void h1();
    //@ assigns \nothing;
    extern void h2();
    //@ assigns \nothing;
    extern void h3();
    //@ assigns \nothing;
    extern void h4();
    
    typedef void (*T_FUN)(void);
    const T_FUN t[]={h0,h1,h2,h3,h4};
    
    void f() {
        int i;
        for (i=0;i<5;i++) (*t[i])();
    }
    
    c file icon fptr.c (322 bytes) 2011-03-21 17:18 +

-Relationships
related to 0001026closedyakobowski value analysis memory consumption problem when using -lib-entry option 
+Relationships

-Notes

~0001621

pascal (reporter)

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 (reporter)

Last edited: 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 (reporter)

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 (reporter)

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 (manager)

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 (reporter)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-03-21 17:18 ddelmas New Issue
2011-03-21 17:18 ddelmas Status new => assigned
2011-03-21 17:18 ddelmas Assigned To => pascal
2011-03-21 17:18 ddelmas File Added: fptr.c
2011-03-21 20:57 pascal Category Plug-in > users => Plug-in > value analysis
2011-03-21 20:57 pascal Summary wrong set of calls in lib-entry mode => wrong treatment for const arrays in lib-entry mode
2011-03-21 20:58 pascal Note Added: 0001621
2011-03-21 21:30 pascal Note Added: 0001623
2011-03-21 21:47 pascal Note Edited: 0001623
2011-03-21 21:48 svn
2011-03-21 21:48 svn Status assigned => resolved
2011-03-21 21:48 svn Resolution open => fixed
2011-03-22 11:28 pascal Note Added: 0001626
2011-03-22 11:28 pascal Status resolved => feedback
2011-03-22 11:28 pascal Resolution fixed => reopened
2011-03-22 11:28 pascal Status feedback => confirmed
2011-05-13 22:05 pascal Note Added: 0001893
2012-04-07 23:56 yakobowski Status confirmed => assigned
2012-04-07 23:56 yakobowski Assigned To pascal => yakobowski
2012-04-07 23:57 yakobowski Relationship added related to 0001026
2012-04-08 00:06 yakobowski Target Version => Frama-C Oxygen-2012xx01
2012-04-11 10:26 yakobowski Note Added: 0002857
2012-05-19 17:01 svn
2012-05-19 17:01 svn Status assigned => resolved
2012-05-19 17:01 svn Resolution reopened => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 pascal Source_changeset_attached => framac master b17eefa4
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon b17eefa4
2014-02-12 16:59 pascal Note Added: 0004822
2014-02-12 16:59 pascal Assigned To yakobowski => pascal
2014-02-12 16:59 pascal Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History