| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002284 | Frama-C | Plug-in > E-ACSL | public | 2017-02-24 14:26 | 2017-05-31 19:05 |
|
| Reporter | kvorobyov | |
| Assigned To | signoles | |
| Priority | normal | Severity | crash | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | Linux | OS | Gentoo | OS Version | |
| Product Version | Frama-C 14-Silicon | |
| Target Version | | Fixed in Version | Frama-C 15-Phosphorus | |
|
| Summary | 0002284: E-ACSL type system crash |
| Description | Run:
e-acsl-gcc.sh --rte=mem mesa_error.c
crashes E-ACSL with the following message:
[e-acsl] failure: expected an integral type for (int)((float)(*(red + i) * scale))
Base frama-C command:
frama-c -no-frama-c-stdlib a.c -rte -no-warn-signed-overflow -no-warn-unsigned-overflow -no-warn-signed-downcast -no-warn-unsigned-downcast -rte-no-div -rte-no-float-to-int -rte-mem -rte-no-pointer-call -rte-no-precond -rte-no-shift -rte-no-trivial-annotations -then -e-acsl -then-last -print -ocode a.out.frama.c
Supposedly this happens because integer interval is computed incorrectly due to casts
|
| Tags | No tags attached. |
|
| Attached Files |  mesa_int_.c [^] (269 bytes) 2017-02-24 14:26 [Show Content] [Hide Content]struct gl_pixel_attrib {
float MapRtoR[256] ;
};
static void map_rgba(struct gl_pixel_attrib *attr, float red[]) {
float rscale = 0.1;
int i = 0;
red[i] = attr->MapRtoR[ (int) (red[i] * rscale) ];
}
int main(int argc, const char *argv[]) {
return 0;
}
|
|
Relationships 
Relationships