Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000759Frama-CPlug-in > value analysispublic2011-03-21 17:182014-02-12 16:59
Reporterddelmas 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filesc file icon fptr.c [^] (322 bytes) 2011-03-21 17:18 [Show Content]

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

-  Notes
(0001621)
pascal (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (manager)
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 (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- 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:15 pascal Note Added: 0001622
2011-03-21 21:26 pascal Note Deleted: 0001622
2011-03-21 21:30 pascal Note Added: 0001623
2011-03-21 21:47 pascal Note Edited: 0001623
2011-03-21 21:48 svn Checkin
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 Checkin
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
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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker