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] Evaluation of an expression?
- Subject: [Frama-c-discuss] Evaluation of an expression?
- From: dmentre at linux-france.org (David MENTRE)
- Date: Mon, 9 Jan 2012 09:21:17 +0100
Hello, In a course, I would like to illustrate how one can control precision of Frama-C value analysis. I'm using following example: """ int x, y, z; void main(int c) { x = c ? 0 : 1; y = x ? 0 : 1; z = 10 / (x - y); } """ I'm using Frama-C Nitrogen or Carbon (depending of the machine). In both cases, I'm calling Frama-C with: frama-c-gui -val possible-zero.c and frama-c-gui -val -slevel 2 possible-zero.c In the second case, the assertion "(x - y) != 0" is not inserted, which is I wanted. However, if I do "Evalute expression" at "z = ..." for "x - y", I get {-1; 0; 1; }. I would have expected {-1; 1;} as the assertion is not inserted. Any explanation? Best regards, david
- Follow-Ups:
- [Frama-c-discuss] Evaluation of an expression?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Evaluation of an expression?
- Prev by Date: [Frama-c-discuss] New Frama-C Plug-in: E-ACSL
- Next by Date: [Frama-c-discuss] Evaluation of an expression?
- Previous by thread: [Frama-c-discuss] New Frama-C Plug-in: E-ACSL
- Next by thread: [Frama-c-discuss] Evaluation of an expression?
- Index(es):