0000825: r13465, crash in slicing (csmith) - Frama-C Bug Tracking System

(0001896)
Anne (reporter)
2011-05-16 09:05

[Db.Value.condition_truth_value] returned (false, false), and we saw that it can happen when the statement is not registered in [Db.Conditions_table].
But when does that happen more precisely ?

(0001897)
Anne (reporter)
2011-05-16 09:27
edited on: 2011-05-16 09:31

I have found why : the statement seems unreachable... but both branches are reachable through [goto] statements.

(0001898)
pascal (reporter)
2011-05-16 10:50

Another possibility is that for all paths explored by the value analysis, the evaluation of the condition ends in run-time error. The programs generated by Csmith are supposed to be well-defined but 1) I have reported several bugs where they weren't 2) the if can be unreachable in reality, and appear to be reached in the value analysis with values that make the condition produce a run-time error.

(0001899)
pascal (reporter)
2011-05-16 11:02

Actually, generation of "gotos" was supposed to be disabled when producing this example, so the gotos would have been generated by CIL and similar situations are likely to come up again often in programs written with a lot of && and ||.

(0001900)
Anne (reporter)
2011-05-16 13:30

Yes : I suppose you are right. People are not supposed to write unreachable code, but it might happen...

(0004787)
Anne (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2011-05-14 01:44	pascal	New Issue
2011-05-14 01:44	pascal	Status	new => assigned
2011-05-14 01:44	pascal	Assigned To	=> Anne
2011-05-14 01:44	pascal	File Added: c.tgz
2011-05-14 01:45	pascal	Summary	r13465, crash in slicing => r13465, crash in slicing (csmith)
2011-05-16 09:05	Anne	Note Added: 0001896
2011-05-16 09:27	Anne	Note Added: 0001897
2011-05-16 09:31	Anne	Note Edited: 0001897
2011-05-16 10:50	pascal	Note Added: 0001898
2011-05-16 11:02	pascal	Note Added: 0001899
2011-05-16 13:30	Anne	Note Added: 0001900
2011-05-16 14:01	svn	Checkin
2011-05-16 14:01	svn	Status	assigned => resolved
2011-05-16 14:01	svn	Resolution	open => fixed
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed
2014-02-12 16:59	Anne	Note Added: 0004787
2014-02-12 16:59	Anne	Status	closed => resolved

Notes
(0001896) Anne (reporter) 2011-05-16 09:05	[Db.Value.condition_truth_value] returned (false, false), and we saw that it can happen when the statement is not registered in [Db.Conditions_table]. But when does that happen more precisely ?

(0001897) Anne (reporter) 2011-05-16 09:27 edited on: 2011-05-16 09:31	I have found why : the statement seems unreachable... but both branches are reachable through [goto] statements.

(0001898) pascal (reporter) 2011-05-16 10:50	Another possibility is that for all paths explored by the value analysis, the evaluation of the condition ends in run-time error. The programs generated by Csmith are supposed to be well-defined but 1) I have reported several bugs where they weren't 2) the if can be unreachable in reality, and appear to be reached in the value analysis with values that make the condition produce a run-time error.

(0001899) pascal (reporter) 2011-05-16 11:02	Actually, generation of "gotos" was supposed to be disabled when producing this example, so the gotos would have been generated by CIL and similar situations are likely to come up again often in programs written with a lot of && and \|\|.

(0001900) Anne (reporter) 2011-05-16 13:30	Yes : I suppose you are right. People are not supposed to write unreachable code, but it might happen...

(0004787) Anne (reporter) 2014-02-12 16:59	Fix committed to stable/neon branch.

Relationships