GNU.WIKI: The GNU/Linux Knowledge Base

  [HOME] [PHP Manual] [HowTo] [ABS] [MAN1] [MAN2] [MAN3] [MAN4] [MAN5] [MAN6] [MAN7] [MAN8] [MAN9]

  [0-9] [Aa] [Bb] [Cc] [Dd] [Ee] [Ff] [Gg] [Hh] [Ii] [Jj] [Kk] [Ll] [Mm] [Nn] [Oo] [Pp] [Qq] [Rr] [Ss] [Tt] [Uu] [Vv] [Ww] [Xx] [Yy] [Zz]


NAME

       victor  -  attempts  to  discharge  verification  conditions  using SMT
       solvers

SYNOPSIS

       victor [UNIT]

DESCRIPTION

       The victor command is a wrapper around ViCToR  (vct)  which  simplifies
       its  use.  ViCToR  translates SPARK verification conditions into SMTlib
       and feeds them to an SMT solver. SPARK ships with one such SMT  solver,
       alt-ergo, but it is possible to use others solvers such as cvc3.

       The  intended  use  of victor is to discharge true VCs left over by the
       Simplifier and not replace the Simplifier. Please also note that ViCToR
       is considered to be an experimental feature at the moment.

       This  manual page only summarises the victor command-line flags, please
       refer to the full VictorWrapper manual for further information.

OPTIONS

       These options do not quite follow the usual GNU command line syntax  as
       options start with a single dash instead of the usual two.

       -h, -help
              Shows command-line help.

       -t=SECONDS
              Time-out  the  SMT solver after this many seconds (by default 5)
              using ulimit. To disable time-out specify 0.

       -m=MEGABYTES
              Limit the SMT solver to this many  MiB  of  virtual  memory  (by
              default no limit) using ulimit.

       -v     Ignore the presence of any siv files and process vcg files only.
              By default, given a UNIT such as foo, victor will first  attempt
              to process foo.siv and then fall back to foo.vcg.

       -plain Plain mode — supress timings and versions.

       -solver=SOLVER
              Specifies an alternative SMT solver. By default we use alt-ergo.
              Can be one of alt-ergo, cvc3, yices or z3. The  alt-ergo  solver
              is  distributed  with  SPARK. The cvc3 solver is part of Debian.
              The yices and z3 solvers are proprietary.

SEE ALSO

       spark(1), sparksimp(1), spadesimp(1), zombiescope(1), pogs(1)

       sparkformat(1), sparkmake(1)

       cvc3(1)

AUTHOR

       This    manual    page    was    written     by     Florian     Schanda
       <florian.schanda@altran-praxis.com>  for  the  Debian  GNU/Linux system
       (but may be used by others). Permission is granted to copy,  distribute
       and/or   modify   this  document  under  the  terms  of  the  GNU  Free
       Documentation License, Version 1.3 or any later  version  published  by
       the  Free  Software  Foundation;  with no Invariant Sections, no Front-
       Cover Texts and no Back-Cover Texts.

                                 22 March 2011                       victor(1)



  All copyrights belong to their respective owners. Other content (c) 2014-2018, GNU.WIKI. Please report site errors to webmaster@gnu.wiki.
Page load time: 0.118 seconds. Last modified: November 04 2018 12:49:43.