Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001486Frama-CPlug-in > value analysispublic2013-09-26 13:272014-03-13 15:57
Reporterdpariente 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 [Show Content]

- Relationships

-  Notes
(0004100)
yakobowski (manager)
2013-09-26 17:57

The bugs is not related to abstract struct:


struct s {
  int *f1;
};

//@ requires \valid(p->f1);
void f(struct s *p) {
}
(0004101)
yakobowski (manager)
2013-09-26 18:03

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.

- 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 Checkin
2013-09-26 18:43 svn Status assigned => resolved
2013-09-26 18:43 svn Resolution open => fixed
2013-09-27 08:55 svn Checkin
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker