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

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