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: Predicate not taking constraints from requires?

  • Subject: [Frama-c-discuss] WP: Predicate not taking constraints from requires?
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Tue, 11 Feb 2014 08:24:15 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7660449BB@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449BB@Mail1.FCMD.local>
Hi,

Since your predicate is used into an ensures clause,
the value that have to be used for  nPULSEOX_MAX_VALUE
is the one of the variable at the post-state of the function.

Since you didn't write an assign clause, the value 100 cannot
be used:  nPULSEOX_MAX_VALUE may be modified by your function.

Patrick.

Le 10/02/2014 22:09, Dharmalingam Ganesan a ?crit :
> Hi,
>
> I got a predicate as follows:
>
> predicate SaO2AboveMaxLimit = mfSaO2 > nPULSEOX_MAX_VALUE;
>
>
> However, below this predicate I defined the
>
> /*@
>     requires nPULSEOX_MAX_VALUE == 100;
>    
>
>     behavior HighSaO2: // SaO2 exceeds max
>      assumes !Adv_or_Mon_Failed;
>      assumes PRU_Is_Off;
>      ensures SaO2AboveMaxLimit ==> DataInvalid;
>
> */
>
>
> I was thinking that when the predicate is used from the ensures block, nPULSEOX_MAX_VALUE  of 100 will be used in the evaluation of mfSaO2 > 100.
>
> But it seems that constraints placed in the requires are not in the scope of predicates that are called from ensures, for example. That is, nPULSEOX_MAX_VALUE == 100 is not taken into consideration I think.
>
> Any comments?
>
> Thanks,
> Dharma
> ________________________________________
> From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Lo?c Correnson [loic.correnson at cea.fr]
> Sent: Monday, February 10, 2014 9:58 AM
> To: Frama-C public discussion
> Subject: Re: [Frama-c-discuss] WP: Pointer issue?
>
> I can only say: soon ;-)
>
> Le 10 f?vr. 2014 ? 15:48, Dharmalingam Ganesan <dganesan at fc-md.umd.edu<mailto:dganesan at fc-md.umd.edu>> a ?crit :
>
> Ok, thanks a lot. Any idea when the future release will be out?
>
> -----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
> 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
> 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>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> .
>


-- 
Patrick Baudin, DILS/LSL, B?t. 862,
Point Courrier n? 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072