Hi,

This is the first time I hear about the Astraver project and it looks very
interesting. The only documents I could find in English about it are the
release notes for the 1.0 and 1.1 versions (in early 2015 and late 2016):

  http://linuxtesting.org/18-02-2015
  http://linuxtesting.org/30-11-2016

Would you have a pointer to a more general description of the project? Is
there a blog that can be followed?
>From the Changelog, it looks like you are adapting Frama-C + Jessie to
scale to linux kernel sources. Is there a subset of the sources that you
can currently verify, and what is the goal? Could we see at some point, for
example, patches containing ACSL formulas integrated in the upstream kernel?

Cheers

On Wed, Aug 9, 2017 at 3:58 PM, Denis Efremov <efre...@ispras.ru> wrote:

> Hello! This is the prototype for prove tool (why3prove analog) based on
> strategies with session handling.
>
> Differences between why3prove and why3sprove:
> 1. Sprove works with existing sessions
> 2. Sprove creates session if it's not exists
> 3. Sprove saves its results to the session
> 4. Sprove supports strategies
>
> Motivation: sprove automatically proves most of the vc's with an
> appropriate strategy without requiring manual interaction with the ide.
> This allows, for example, to use frama-c (jessie plugin) with why3 in
> cli mode.
>
> This patch is developed as a part of the AstraVer
> (http://linuxtesting.org/astraver) project.
>
> Usage: why3 sprove [options] -S <strategy> [file|-]
>   -C <file>                read configuration from <file>
>   --config                 same as -C
>   --extra-config <file>    read additional configuration from <file>
>   -L <dir>                 add <dir> to the library search path
>   --library                same as -L
>   --debug <flag>           set a debug flag
>   --debug-all              set all debug flags that do not change Why3
> behaviour
>   --list-debug-flags       list known debug flags
>   -S <strategy>            use strategy to prove goals.
> By default, the strategy will be scheduled on all goals.
> You can limit scheduling with select and filter options.
> Select and filter can't be applied on the same level simultaneously.
>   --strategy               same as -S
>   --clean                  remove failed proof attempts before exit
>   --file-filter <string>   don't run strategy on files with id string
> (case insensitive)
>   --theory-filter <string> don't run strategy on theories with id string
> (case insensitive)
>   --goal-filter <string>   don't run strategy on goals with id string
> (case insensitive)
>   --file-select <string>   run strategy on files with id string (case
> insensitive)
>   --theory-select <string> run strategy on theories with id string (case
> insensitive)
>   --goal-select <string>   run strategy on goals with id string (case
> insensitive)
>   --extra-expl-prefix <s>  register s as an additional prefix for VC
> explanations
>   -h                       print this list of options
>   --help                   same as -h
>
> Usage example:
> $ cd examples/
> $ rm -fr swap
> $ why3 sprove --strategy "Auto level 1" swap.mlw
> [SPROVE] found regular file 'swap.mlw'
> [SPROVE] using 'swap' as directory for the project
> [SPROVE session] Opening session...
>
> [SPROVE session] Opening session: update done
>
> [SPROVE session] Opening session: done
> [SPROVE] Strategy 'Auto level 1' loaded.
> [SPROVE] Strategy 'Compute' loaded.
> [SPROVE] Strategy 'Inline' loaded.
> [SPROVE] Strategy 'Inline all' loaded.
> [SPROVE] Strategy 'Intro premises' loaded.
> [SPROVE] Strategy 'Split' loaded.
> [SPROVE] Strategy 'proof_juicer' loaded.
> [SPROVE session] Adding file '../swap.mlw'
> [SPROVE] adding file ../swap.mlw in database
> File 'swap.mlw' verified: false
> sheduling strategy on goal: WP_parameter swap (1. VC for swap)
> sheduling strategy on goal: WP_parameter swap (1. VC for swap)
> sheduling strategy on goal: WP_parameter swap_ref (2. VC for swap_ref)
> Proof with 'Z3 4.5.0' gives Valid 0.05 [1.0]
> Goal 'WP_parameter swap_ref' proved: true
> Proof with 'Z3 4.5.0' gives Valid 0.05 [1.0]
> Goal 'WP_parameter swap' proved: true
> Theory 'SwapInt32' verified: true
> Proof with 'Z3 4.5.0' gives Valid 0.03 [1.0]
> Goal 'WP_parameter swap' proved: true
> Theory 'Swap' verified: true
> File 'swap.mlw' verified: true
>
> Saving session... done
>  3/3 %
> ------------------------------------------------------
>
> Integration with Frama-C (AstraVer version of Jessie plugin):
> $ frama-c -jessie -jessie-target why3ml -jessie-why3-opt "sprove -S
> proof_juicer --clean --theory-filter axiom" swap.c
>
> Patch on github:
> https://github.com/evdenis/why3/commit/fe8161a99073af7bf38531bca6f882
> a1b230a171
>
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Reply via email to