kernel generates UnspecifiedSequence when 2 following ternary operators

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

---

Id	Project	Category	View	Due Date	Updated
ID0002435	Frama-C	Kernel	public	2019-05-07	2019-05-08

Reporter	rmalak	Assigned To	virgile	Resolution	open
Priority	normal	Severity	major	Reproducibility	always
Platform	x86_64 Linux 4.19	OS	OCaml 4.07.1 Opam 2.0.3	OS Version	Debian Sid
Product Version	Frama-C 18-Argon	Target Version	-	Fixed in Version	-

Description :

Consider ternary_operator.c :

///////////////// int main() { return (2>1) ? 1 : (1>0) ? 1 : 0; } /////////////////

then frama-c generates :

///////////////// int main(void) { int tmp_0; if (2 > 1) tmp_0 = 1; else { int tmp; if (1 > 0) tmp = 1; else tmp = 0; tmp_0 = tmp; } return tmp_0; } //////////////

and considers :

if (1 > 0) tmp = 1; else tmp = 0; tmp_0 = tmp;

as an UnspecifiedSequence statement

if (1 > 0) tmp = 1; else tmp = 0;

as a "If" statement

and

tmp_0 = tmp;

as a "Instr" statement

Is the construction of the AST with a intermediate UnspecifiedSequence the normal behaviour ?

Attachments

• ternary_operators.c