Plug-in crash with "Unregistered_library_function" error
ID0002192: This issue was created automatically from Mantis Issue 2192. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002192 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2018-11-30 |
| Reporter | kvorobyov | Assigned To | kvorobyov | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C 14-Silicon |
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 Information :
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.