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: WP issues
- Subject: [Frama-c-discuss] Frama-c: WP issues
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- Date: Wed, 15 Jan 2014 11:35:29 -0500
- In-reply-to: <52D6B7B0.4020005@fr.merce.mee.com>
- References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local> <52D6B7B0.4020005@fr.merce.mee.com>
Hello, Thanks for your response. There are no loops in the code. I do not know whether you had a chance to see the stackoverflow link I gave. According to a developer of alt-ergo (0.95), he thinks this behavior is valid for Oxygen (after he fixes syntax errors in the generated why/mlw code). This behavior is reported as unknown for the newest version Fluorine. Best regards, Dharma -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David MENTRE Sent: Wednesday, January 15, 2014 11:31 AM To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Frama-c: WP issues Hello, Le 13/01/2014 21:47, Dharmalingam Ganesan a ?crit : > 2.http://cp.mcafee.com/d/1jWVIi4x0e6jqbbNEVuKOM-yrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCPhOg74744T-LP3yb0VctRXBQhNEVLMWX5PhO-ZORQr8FGTsvVkffGhBrwqrhdICXYyMCY-ehojd79KVI07iuSaRc_5Q-FzBY5C_FelokNd6XbBPhOZxxoKIuShB0KoBcCnQ-pvUAqBSUqgfYLeFtqdjfCToWHFuNt2lbdQEn8lrxrW0E-l9QUyW01_FgzbutyrosvpdwLQzh0qmNueGWnIngBiPta6BQQg2YtlQLp8Qg0a5zh1aB6_ErKrHo1j > You said: > This behavior should be true because there is no other place tenumRMode is updated except the first conditional statement's else section. > > The wierd thing is that if I comment some lines arbitrarily I always get "valid" from Alt-ergo. Have you some loop in the commented out code? You can also add "assert tenumRMode == SS_A_MODE;" at various points in your code to see where WP is failing to prove it. Best regards, david -- David MENTR? - Research engineer, Ph.D. Formal Methods and tools MITSUBISHI ELECTRIC R&D Centre Europe (MERCE) Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59 http://cp.mcafee.com/d/5fHCN8SyOYqenHIIfECXCQXL8LccfEFCQXL8LccfKcCQXL8LccfEI6QXL9KnojujdE4txZdw2Dr5RkerlgXQ6PrJyWG7dGEtW3pIQsA1N1N1d_HYMUyMej7tuVt4sqerYeKNsQsLLsJt6OaqJT7-l3PWApmU6CQPr9K_8I9LfzAm4PhOrKr01eNVmkWdA9k9OY_XjzaNudLXSPrItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdIefICMnWhEwdboL7ltbSbEiFpKB3iWq81ueGWnIAq8052NEwBizvQdTdLIN95CiyA54 _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://cp.mcafee.com/d/k-Kr41Aq6x0SyOYqenHIIfECXCQXL8LccfEFCQXL8LccfKcCQXL8LccfEI6QXL9KnojujdE4txZdw2Dr5RkerlgXQ6PrJyWG7dGEtW3pIQsA1N1N1d_HYMUyMej7tuVt4sqerYeKNsQsLLsJt6OaqJT7-l3PWApmU6CSjr9K_8I9LfzAm4PhOrKr01DOFeD4ng0fZa4prPIs0gKgB31dnoovaAVgtHzItlQLoKxaBCWkdKNRniZyW4GmrFgKgGT2TQ1hYGjFN5Q03_ix6mYX4SMU-Or1vF6y0QJyYtlQLoKxaBCWkdbFEw5UWHFuOhEw0kb6y2lad_gTsS3uiuEOT
- Follow-Ups:
- [Frama-c-discuss] Frama-c: WP issues
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Frama-c: WP issues
- References:
- [Frama-c-discuss] Frama-c: WP issues
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Frama-c: WP issues
- From: d.mentre at fr.merce.mee.com (David MENTRE)
- [Frama-c-discuss] Frama-c: WP issues
- Prev by Date: [Frama-c-discuss] Frama-c: WP issues
- Next by Date: [Frama-c-discuss] Frama-c: WP issues
- Previous by thread: [Frama-c-discuss] Frama-c: WP issues
- Next by thread: [Frama-c-discuss] Frama-c: WP issues
- Index(es):