Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- Subject: [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- From: eric.liu at uniquesoft.com (Eric Liu)
- Date: Mon, 12 Jul 2010 18:23:15 +0800
Hi, Frama-C folks: I am using Frama-C Boron-20100401 on Ubuntu 10.04. When I am trying "Undefined side-effects in expressions" feature, I find Frama-C does not complain it. However, the user manual says Frama-C will produce such warning message. se.c :5: ... undefined multiple accesses in expression . assert \ s e p a r a t e d (& x ,& x); se.c :7: ... undefined multiple accesses in expression . assert \ s e p a r a t e d (& x,p); Here is my test code, called with parameter c = 1. void UnspecifiedSideEffectInExpression(int c) { int x = 0, y = 0, z = 20, t = 30, *p, *q; if (c & 1) { x = c; y = (x++) + (x++); } printf("x = %d, y = %d\n", x, y); p = c&2 ? &x : &t; printf("*p = %d\n", *p); y = *p + x++; printf("y = %d\n", y); q = c&4 ? &z : &t; printf("*q = %d\n", *q); y = *q + x++; printf("x= %d, y = %d, z = %d, t = %d\n", x, y, z, t); } int main() { UnspecifiedSideEffectInExpression(1); return 0; } Can anyone point me out why I can't get the warning message. My command line is "frama-c -val myfile.c". Thanks Eric
- Follow-Ups:
- [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- Prev by Date: [Frama-c-discuss] *p and p[0]
- Next by Date: [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- Previous by thread: [Frama-c-discuss] Pointer problem with nested objects
- Next by thread: [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- Index(es):