Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002284Frama-CPlug-in > E-ACSLpublic2017-02-24 14:262017-05-31 19:05
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformLinuxOSGentooOS Version
Product VersionFrama-C 14 Silicon 
Target VersionFixed in VersionFrama-C 15 Phosphorus 
Summary0002284: E-ACSL type system crash
DescriptionRun:

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
TagsNo tags attached.
Attached Filesc file icon mesa_int_.c [^] (269 bytes) 2017-02-24 14:26 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-02-24 14:26 kvorobyov New Issue
2017-02-24 14:26 kvorobyov Status new => assigned
2017-02-24 14:26 kvorobyov Assigned To => signoles
2017-02-24 14:26 kvorobyov File Added: mesa_int_.c
2017-02-27 11:15 signoles Status assigned => resolved
2017-02-27 11:15 signoles Resolution open => fixed
2017-05-31 19:04 signoles Fixed in Version => Frama-C 15 Phosphorus
2017-05-31 19:05 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker