--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on January 2014 ---
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