GitLab

ID0001945: This issue was created automatically from Mantis Issue 1945. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001945	Frama-Clang	Plug-in > clang	public	2014-10-30	2015-02-17

Reporter	Jochen	Assigned To	virgile	Resolution	open
Priority	normal	Severity	text	Reproducibility	always
Platform	frama-c-Neon-20140301+dev-stance	OS	xubuntu-cfe13.10	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	-

Description :

running file 050.cpp (from the resolved issue #1569 (closed)) generates the output:

Now output intermediate result [kernel] warning: Assuming declared function malloc can't throw any exception

In the long run, this warning should be avoided, since it is confusing to novel users. All methods (such as malloc) that don't originate from C++ user input should be handled as known to Frama-C.

According to Stroustrup's "The C++ programming language" (3rd ed.), sect.14.10, "new" may throw the exception "bad_alloc". Frama-C should be aware of this, without telling it to the user every time.

Attachments

• 050.cpp
• 050a.cpp