Frama-C Bug Tracking System - Frama-C
View Issue Details
0002192Frama-CPlug-in > E-ACSLpublic2015-12-04 10:522018-11-30 11:35
kvorobyov 
kvorobyov 
normalminoralways
closedfixed 
 
Frama-C 14-Silicon 
0002192: Plug-in crash with "Unregistered_library_function" error
/** 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]);
}
This 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.
No tags attached.
Issue History
2015-12-04 10:52kvorobyovNew Issue
2015-12-04 10:52kvorobyovStatusnew => assigned
2015-12-04 10:52kvorobyovAssigned To => kvorobyov
2015-12-08 13:58signolesNote Added: 0006117
2015-12-08 17:37kvorobyovNote Added: 0006118
2016-09-13 09:19kvorobyovStatusassigned => resolved
2017-01-18 15:09signolesFixed in Version => Frama-C 14-Silicon
2017-01-18 15:09signolesNote Added: 0006343
2017-01-18 15:09signolesStatusresolved => closed
2018-11-30 11:35signolesResolutionopen => fixed

Notes
(0006117)
signoles   
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   
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   
2017-01-18 15:09   
Fixed in E-ACSL 0.8 compatible with Frama-C Silicon.