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] WP: Pointer issue?
- Subject: [Frama-c-discuss] WP: Pointer issue?
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- Date: Thu, 13 Mar 2014 15:27:43 -0400
- In-reply-to: <677BB8C7-77F2-4624-8066-111FE2A8A244@cea.fr>
- References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449B7@Mail1.FCMD.local> <53CBDA4C-83C0-4ED7-889D-448A58174BEA@cea.fr> <B517F47C2F6D914AA8121201F9EBEE6701C766926AEB@Mail1.FCMD.local> <677BB8C7-77F2-4624-8066-111FE2A8A244@cea.fr>
Hi, I tried this example on the latest version of Frama-c (downloaded it last night). I'm not sure why two of the properties are Unknown. Please let me know. Thanks, Dharma $ frama-c -wp -wp-rte -wp-proof=alt-ergo pointer.c -pp-annot -wp-model=Typed,ref [kernel] preprocessing with "gcc -C -E -I. -dD pointer.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function f [rte] annotating function main [wp] Collecting variable usage [wp] 11 goals scheduled [wp] [Qed] Goal typed_ref_f_assign : Valid [wp] [Qed] Goal typed_ref_f_p_changed_post : Valid [wp] [Qed] Goal typed_ref_f_p_changed_post_2 : Valid [wp] [Qed] Goal typed_ref_f_q_changed_post : Valid [wp] [Qed] Goal typed_ref_f_q_changed_post_2 : Valid [wp] [Alt-Ergo] Goal typed_ref_f_assert_rte_mem_access_2 : Unknown [wp] [Alt-Ergo] Goal typed_ref_f_assert_rte_mem_access : Unknown [wp] [Qed] Goal typed_ref_main_call_f_q_changed_pre : Valid [wp] [Qed] Goal typed_ref_main_call_f_p_changed_pre_2 : Valid [wp] [Alt-Ergo] Goal typed_ref_main_call_f_p_changed_pre : Valid (28ms) (13) [wp] [Alt-Ergo] Goal typed_ref_main_call_f_q_changed_pre_2 : Valid (Qed:4ms) (80ms) (43) [wp] Proved goals: 9 / 11 Qed: 7 (4ms-4ms) Alt-Ergo: 2 (28ms-80ms) (43) (unknown: 2) -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr> [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Lo?c Correnson Sent: Monday, February 10, 2014 9:36 AM To: Frama-C public discussion Subject: Re: [Frama-c-discuss] WP: Pointer issue? This is ok in the future release : f is fully proved. However, let me point out that the specification of `f` is far from complete. Especially, since there is no assigns nor specification for both p and q in all behaviors, then the main function can not be proved. You probably have to : + assigns *p,*q ; in default behavior + ensures *p == \old(*p) ; in q_changed behavior ensures *q == \old(*q) + ; in p_changed behavior L. Le 7 f?vr. 2014 ? 21:37, Dharmalingam Ganesan <dganesan at fc-md.umd.edu<mailto:dganesan at fc-md.umd.edu>> a ?crit : Hi, For the attached program, I'm not sure why the requires clause is not valid for "q_changed". behavior q_changed: assumes n <= 0; requires \valid(q); ensures *q == n; Any comments? Thanks, Dharma ________________________________________ From: frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr> [frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr>] On Behalf Of David Cok [dcok at grammatech.com<mailto:dcok at grammatech.com>] Sent: Friday, February 07, 2014 12:12 PM To: frama-c-discuss at lists.gforge.inria.fr<mailto:frama-c-discuss at lists.gforge.inria.fr> Subject: Re: [Frama-c-discuss] Checking for side-effects I understand it differently. See section 2.3.2 of the ACSL documentation. The semantics of the assigns clause is that only the listed locations may be updated. Anything not listed is assumed to be the same in the post-state and the pre-state. Anything listed may or may not be assigned to in the method. This is consistent with the interpretation in JML as well. Having no assigns clause imposes no restrictions, so the default is equivalent to something like assigns \everything - though section 2.3.5 allows tools to do something more intelligent. I can't speak either way to whether frama-c reports violations of assigns clauses or has a bug relating to them. - David On 2/7/2014 10:12 AM, Dharmalingam Ganesan wrote: Hi, In my understanding assigns clause is for ensuring the given variables are updated. If the code assigns additional variables that are not listed in the assign clause, then WP is not reporting as an issue. I understand that's ok, but my question is different: Can we specify only a given set of variables are allowed to be modified and nothing else? Of course, for small programs we can add additional constraints such as dummy == \old(dummy), for example. But this workaround becomes an issue if the code has "too many" variables, we have to manually add such constraints for each variable that should not be modified. Thanks, Dharma -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr> [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David Cok Sent: Friday, February 07, 2014 9:58 AM To: frama-c-discuss at lists.gforge.inria.fr<mailto:frama-c-discuss at lists.gforge.inria.fr> Subject: Re: [Frama-c-discuss] Checking for side-effects Isn't this what the 'assigns' clause is for? As in /*@ requires global == dummy; behavior GLOBAL_BELOW_5: assumes global < 5; assigns global; ensures global == \old(global) + 1; behavior GLOBAL_ABOVE_5: assumes global > 5; assigns global; ensures global == \old(global) - 1; behavior GLOBAL_EQUAL_5: assumes global == 5; assigns \nothing; complete behaviors; disjoint behaviors; */ - David On 2/6/2014 2:47 PM, Dharmalingam Ganesan wrote: Hi, Is there a way to specific "negative" behaviours, for example, no variable should be updated except the given variable. For example, for this little code, WP can able to prove all behaviours. That's great. But, I do not want any change in the state of the system except the "global" value. In this code, the dummy variable's state can also change, which is an undesirable side-effect (let's assume). For large and complex code, it appears specifying what is not allowed would also help to make sure implementation = specification. I looked into -deps option to Frama-c, it appears to list the dependencies for each variable, which is helpful, but it does not quite check for undesired state changes. Any comments? Dharma int global = 0; int dummy = 0; /*@ requires global == dummy; behavior GLOBAL_BELOW_5: assumes global < 5; ensures global == \old(global) + 1; behavior GLOBAL_ABOVE_5: assumes global > 5; ensures global == \old(global) - 1; behavior GLOBAL_EQUAL_5: assumes global == 5; assigns \nothing; complete behaviors; disjoint behaviors; */ void update() { if(global < 5) { global++; dummy++; } if(global > 5) { global--; dummy--; } } _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://cp.mcafee.com/d/avndy0Od20Qrhpd7a8VVZ55MTsSDtV5VxxZ5cSDtV5Vxx ZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdA3hOMWMW C_R-p79L3HZuVtdCUXDNP1EVupVqWdAklkkk-l3PWApmU6CQjqpK_8I9LfzAm4PhOrKr 01DOFeD4ng0fZa4prPIs0gKgB31dnoovaAVgtHzItlQLoKxaBCWkdKNRniZyW4GmrFgK gGT2TQ1hYGjFN5Q03_ix6mYX4S-qekhNI5-Aq83iSbNRniZyW4GmrFgQKCy0i9_oHa14 QgeRyq8aigYLXHLSDgSMedSnK1T1nG _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://cp.mcafee.com/d/k-Kr3x8SyOqekhPPWabxKVJeXObP33WapJeXObP33Xz9Je XObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSr86zBxRxRd_HYOe ju7nWZOWrdNTfzC3hOYPORQr8EGEEFYG7DR8OJMddFCQPt-hojuv78I9CzATsS03fBite 8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2z VkDjybE07-B2cJVS9JYQsEzzobZ8Qg6BInzGKBX5Q9kITixFtd40Aj-Nmk29EwtH4QgkA xVvTnvJexJwsrhs5CczSf _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://cp.mcafee.com/d/k-Kr6h0SyOqekhNEVphd7apKVJeXObP33WapJeXObP33Xz 9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSrsjohvtjvW_f ffCzAtRXBQnbKsy-CDtPBHFShjlKCVOEuvkzaT0QSyrodTV5xdVYsyMCqejtPo0c-l9QU yW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-waf Bite8Kw0vWk8OTDoCTzhPtYS2_id41Fr5UWHFuNt2lbdQEqnjh094_IlB0yq87qNd4598 unZRTXjEro76TxYp _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://cp.mcafee.com/d/2DRPoOrhpd7a8UQsIECzBcTsSDtV5VxxZ5cSDtV5VxxZNAS DtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdK9I8LKFLZvDDDP hOeWZOWbBTehvjjKVORQX8FGTjsVkffGhBrwqrjdI6XYyMCY-ehojd79KVI06vaAWsht00 _QEhBLeNM12V2kc4RtxxYGjB1SKeNRniZyW4GmrFgSX7ltbSbEiFpKB2V2Hsbvg57OFeD4 ng0fZa4prPIjrNEVK-r1vF6y0QJyYtlQLoKxaBCWkdbFEw4yvSaOwhd43JoCy2AAfb-WXZ FQdI3zvp0rIS2j <pointer.c>_______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://cp.mcafee.com/d/avndygA920Orhpd7atS6rLndTdFTuhuoovhjdFTuhuoovsp dFTuhuoovhodFTujsKMCYCrg8X3Wr05eSbGEsSGxTEdCTr5RkerlgXQ6Prz37LeFLZvCn3 hPuXbTnKnjpKqeuvo76zB6VEVVqWdAklrzCel3PWApmU6CQjrxK_8I9LfzAm4PhOrKr01D OFeD4ng0fZa4prPIs0gKgB31dnoovaAVgtHzItlQLoKxaBCWkdKNRniZyW4GmrFgKgGT2T Q1hYGjFN5Q03_ix6mYX4Syy-YqejobZ8Qg6BInzGKBX5Q9kITixFtd402xp8Qg1qIEj-9E wBizvAzr5Pq8n3bZrc _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://cp.mcafee.com/d/k-Kr43qb9EVjKMPtWVKVJeXObP33WapJeXObP33Xz9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSrsooZVRd_HYOUqerTpuWZOWrdPhPPX0UQsETd7fbnhIyyHssNOEuvkzaT0QSCrsdTV5xdVYsyMCqejtPo0c-l9QUyW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCQknTzhOr1vF6y0QJyYtlQLoKxaBCWkdbFEw0kb96y0blB2vNd44GkrYAroKrKYAj _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss<http://cp.mcafee.com/d/FZsScz8w86QmjhODtxxBZYTsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdTod7fLeFLZvC1PXWbXTnKnjK-VMWUUsYCzORQr8FGEEIYG7DR8OJMddECSjt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JcseppdwLQzh0qmNueGWnIngBiPta6BQQg0a5Azh05GOxfUCy2lad-idIndMjrR> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140313/bc262ce1/attachment-0001.html>
- Prev by Date: [Frama-c-discuss] E-ACSL v0.3
- Next by Date: [Frama-c-discuss] WP Question/Bug?
- Previous by thread: [Frama-c-discuss] WP Question/Bug?
- Next by thread: [Frama-c-discuss] New release Jessie/Why 2.34
- Index(es):