Frama-C Bug Tracking System - Frama-C
View Issue Details
0000388Frama-CPlug-in > Evapublic2010-02-01 15:092014-02-12 16:56
Reporteryakobowski 
Assigned Tomonate 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000388: Incorrect 'assert false' in value analysis
DescriptionThis might be related to variadic calls, but I'm not really sure.

The crash is triggered by the following code:

typedef void *va_list;

#define va_start(AP, LASTARG) \
 (AP = ((va_list) __builtin_next_arg (LASTARG)))


void main(const char *pszMessage,...) {
  va_list vlParameters;
  va_start(vlParameters,pszMessage);
}
Additional InformationSVN 7571
TagsNo tags attached.
Attached Files

There are no notes attached to this issue.

Issue History
2010-02-01 15:09yakobowskiNew Issue
2010-02-01 15:09yakobowskiStatusnew => assigned
2010-02-01 15:09yakobowskiAssigned To => pascal
2010-02-01 20:07monateAssigned Topascal => monate
2010-02-01 20:07monateStatusassigned => resolved
2010-02-01 20:07monateResolutionopen => fixed
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in Version => Frama-C Boron
2013-12-19 01:14Source_changeset_attached => framac master d3208150
2014-02-12 16:56Source_changeset_attached => framac stable/neon d3208150
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva