Frama-C-discuss mailing list archives

loic.correnson at cea.fr (Loïc Correnson) · Wed, 28 Mar 2018 10:12:27 +0200

Hi,

Seems you are on the right way.

I must say that WP is not implementing a schoolbook Â« weakest precondition calculus Â» ; rather, it is a highly optimised and linearised computation
of a formula that, indeed, is probably something between the weakest precondition and the strongest postcondition. See Flanagan, Saxe and Leino papers about efficient WP/SP calculi (and the associated references) for a complete background on this topic.

L.

> Le 27 mars 2018 Ã  14:32, Niklas RosÃ©n <nrosen at kth.se> a Ã©crit :
> 
> Hi
> 
> I have had some limited success using the verification conditions by manually annotating a function with a formula encoded as a postcondition in an ensures clause and then running Wp.VC.generate_kf and Wp.VC.iter_kf or Wp.VC.get_formula to inspect the results. I did not have any success with generate_ip, but maybe I created the property incorrectly somehow. I have revisited this approach and these are some of the issues I run into:
> 
> 1. I would like to use free logical variables in my formulas (essentially placeholders that are not changed by the WP computation). Is it sound to universally quantify these or should I create a new ghost variable for this or what would be an appropriate approach here? 
> 
> 2. I'm having some difficulties programmatically constructing a formula as an ensures clause. It seems I need to add this to a ACSL behavior and so far I have created this using the Cil.mk_behavior function, is this correct? Or should I add this to an existing behavior or create a new one some other way? Also I have not been able to figure out how to properly construct a universal quantification, how do I create the quantified variables, is it enough to create a logic_var record or should these be constructed by some function?
> 
> 3. Even for my minimal examples the verification conditions contain more than the formula I'm trying to generate, e.g. implications of the form (is_sint32 i_4) -> ... which will have to be filtered out again somehow. For simple examples this is trivial to do by hand but I don't know how I would do this algorithmically. There is also the risk of simplifications interfering but I disable most of the simplifications from the command line and I have not yet run into any issues with this.
> 
> All in all, there are a few things I have not figured out how to do in order to get this approach to work well but it may be possible. However, my impression is that it is not very straight forward for what I'm trying to do. I had hoped that it would be possible to use only the WP calculation instead of first setting everything up for generating verification conditions and then try to extract my wanted results.
> 
> As I wrote in my StackOverflow question <https://stackoverflow.com/q/49234253/9479240> I have been looking at the Calculus.Cfg.compute function, would that approach be viable? Or would you recommend that I try solving my issues with using VCs instead?
> 
> 
> Regards,
> Niklas
> 
> From: Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> on behalf of LoÃ¯c Correnson <loic.correnson at cea.fr>
> Sent: Friday, March 23, 2018 16:20
> To: Frama-C public discussion
> Subject: Re: [Frama-c-discuss] Weakest precondition calculation
>  
> Hi
> What about if you pack your formula into an ACSL requires clause, and then ask the WP for generating the associated proof-obligation(s) ?
> You can access those features programmatically via the WPâ€™s API, available online ( API Documentation <http://frama-c.com/download/frama-c-Sulfur-20171101_api.tar.gz> ).
> To starts with, consider using, from module Wp.VC :
> 
> type t 
> elementary proof obligation
> val generate_ip : ?model:string -> Property.t -> t <file:///Users/correnson/Downloads/frama-c-api/wp/Wp.VC.html#TYPEt> Bag.t <file:///Users/correnson/doc/code/html/Bag.html#TYPEt>
> val get_formula : t <file:///Users/correnson/Downloads/frama-c-api/wp/Wp.VC.html#TYPEt> -> Wp.Lang.F.pred <file:///Users/correnson/Downloads/frama-c-api/wp/Wp.Lang.F.html#TYPEpred>
> 
> Regards,
> L.
> 
> 
>> Le 23 mars 2018 Ã  15:37, Niklas RosÃ©n <nrosen at kth.se <mailto:nrosen at kth.se>> a Ã©crit :
>> 
>> Hi
>> 
>> I'm working on my master's thesis and I'm trying to implement an analysis as a plugin to Frama-C. As a part of this analysis I need to generate weakest precondition formulae for a given function and input formula. Could this be done using the WP plugin?
>> 
>> I have asked this question in greater detail at StackOverflow, https://stackoverflow.com/q/49234253/9479240 <https://stackoverflow.com/q/49234253/9479240> , without success so far.
>> 
>> Could anyone shed some light on this or point me in the right direction?
>> 
>> 
>> Best regards
>> Niklas
>> 
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180328/d67668ed/attachment-0001.html>