Frama-C Bug Tracking System - Frama-C
View Issue Details
0001486Frama-CPlug-in > Evapublic2013-09-26 13:272014-03-13 15:57
dpariente 
yakobowski 
normalmajoralways
closedfixed 
Frama-C Fluorine-20130501 
Frama-C Neon-20140301 
0001486: validity of a field defined in an abstract struct typedef
[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?
No tags attached.
? patch-stance (976) 2013-09-26 18:04
https://bts.frama-c.com/file_download.php?file_id=526&type=bug
Issue History
2013-09-26 13:27dparienteNew Issue
2013-09-26 13:27dparienteStatusnew => assigned
2013-09-26 13:27dparienteAssigned To => yakobowski
2013-09-26 17:57yakobowskiNote Added: 0004100
2013-09-26 18:03yakobowskiNote Added: 0004101
2013-09-26 18:04yakobowskiFile Added: patch-stance
2013-09-26 18:43svnCheckin
2013-09-26 18:43svnStatusassigned => resolved
2013-09-26 18:43svnResolutionopen => fixed
2013-09-27 08:55svnCheckin
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0004100)
yakobowski   
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   
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.