2021-02-24 19:16 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001486Frama-CPlug-in > Evapublic2014-03-13 15:57
Reporterdpariente 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001486: validity of a field defined in an abstract struct typedef
Description[STANCE]

The small source code snippet is extracted from an Apache server module.

//------------------------------------
struct core_dir_config { int server_signature; } core_dir_config;
typedef struct core_dir_config core_dir_config;

struct request_rec { struct ap_conf_vector_t *per_dir_config; } request_rec;
typedef struct request_rec request_rec;

//@ requires \valid(r->per_dir_config);
const char * app(request_rec *r)
{
    core_dir_config *conf;
    conf = (core_dir_config *)(((void **)(r->per_dir_config))[0]);
    if (conf->server_signature == 1) { return ""; }
    return " ";
}
//------------------------------------

When analyzed by:
frama-c -val -main app bug.c -lib-entry -no-unicode

Value generates an error:
$ Internal error 835; debug info:
{{ NULL -> {0}; S_r -> {0} }} (size:<32>)

Is it "abstract struct type" related?
Is there any workaround?
TagsNo tags attached.
Attached Files
  • ? file icon patch-stance (976 bytes) 2013-09-26 18:04 -
    Index: src/value/eval_terms.ml
    ===================================================================
    --- src/value/eval_terms.ml	(revision 23860)
    +++ src/value/eval_terms.ml	(working copy)
    @@ -879,7 +879,7 @@
                | [] | _ :: _ :: _ -> raise Not_an_exact_loc
                | [loc] ->
                    let loc = Locations.make_loc loc (Bit_utils.sizeof typ) in
    -               if not (valid_cardinal_zero_or_one ~for_writing:false loc)
    +               if not (cardinal_zero_or_one loc)
                    then raise Not_an_exact_loc;
                    typ, loc
             )
    @@ -1117,7 +1117,7 @@
               let aux typ env lval =
                 try
                   let loc = make_loc lval (Bit_utils.sizeof typ) in
    -              if valid_cardinal_zero_or_one ~for_writing loc then
    +              if cardinal_zero_or_one loc then
                     let state =
                       Eval_exprs.reduce_by_valid_loc ~positive ~for_writing
                         loc typ (env_current_state env)
    
    ? file icon patch-stance (976 bytes) 2013-09-26 18:04 +

-Relationships
+Relationships

-Notes

~0004100

yakobowski (manager)

The bugs is not related to abstract struct:


struct s {
  int *f1;
};

//@ requires \valid(p->f1);
void f(struct s *p) {
}

~0004101

yakobowski (manager)

This is a bug in the evaluation of partially invalid pointers that are required to be valid. All occurrences of valid_cardinal_zero_or_one in src/value/eval_terms.ml must be replaced by calls to cardinal_zero_or_one. A sample patch is attached.
+Notes

-Issue History
Date Modified Username Field Change
2013-09-26 13:27 dpariente New Issue
2013-09-26 13:27 dpariente Status new => assigned
2013-09-26 13:27 dpariente Assigned To => yakobowski
2013-09-26 17:57 yakobowski Note Added: 0004100
2013-09-26 18:03 yakobowski Note Added: 0004101
2013-09-26 18:04 yakobowski File Added: patch-stance
2013-09-26 18:43 svn
2013-09-26 18:43 svn Status assigned => resolved
2013-09-26 18:43 svn Resolution open => fixed
2013-09-27 08:55 svn
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master cdd08e08
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon cdd08e08
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History