Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002192Frama-CPlug-in > E-ACSLpublic2015-12-04 10:522018-11-30 11:35
Reporterkvorobyov 
Assigned Tokvorobyov 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C 14-Silicon 
Summary0002192: Plug-in crash with "Unregistered_library_function" error
Description/** Instrumentation of the following program leads to the plug-in crash with Unexpected error (Misc.Unregistered_library_function("__store_block")) */

#include <stdlib.h>
char *a;
main(char *argv[]) {
    a = argv = atoi(argv[1]);
}
Additional InformationThis error has been extracted by creduce from one of the SPEC CPU2000 179.art benchmark. There seems to be an issue while processing the atoi ACSL contract. This error is triggered in at least 6 more SPEC benchmarks.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006117)
signoles (manager)
2015-12-08 13:58

I guess that using -no-frama-c-stdlib would solve the issue (yet not tried on this particular example).
(0006118)
kvorobyov (developer)
2015-12-08 17:37

I have checked this particular example and also a couple of SPEC benchmarks failing because of this issue. It appears that in the examples that I have used -no-frama-c-stdlib solves the issue but only for the case when -e-acsl-full-mmodel is not used. Once -e-acsl-full-mmodel is specified the failure reappears again.
(0006343)
signoles (manager)
2017-01-18 15:09

Fixed in E-ACSL 0.8 compatible with Frama-C Silicon.

- Issue History
Date Modified Username Field Change
2015-12-04 10:52 kvorobyov New Issue
2015-12-04 10:52 kvorobyov Status new => assigned
2015-12-04 10:52 kvorobyov Assigned To => kvorobyov
2015-12-08 13:58 signoles Note Added: 0006117
2015-12-08 17:37 kvorobyov Note Added: 0006118
2016-09-13 09:19 kvorobyov Status assigned => resolved
2017-01-18 15:09 signoles Fixed in Version => Frama-C 14-Silicon
2017-01-18 15:09 signoles Note Added: 0006343
2017-01-18 15:09 signoles Status resolved => closed
2018-11-30 11:35 signoles Resolution open => fixed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker