GitLab

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.