Dies ist der Befehl victor, der im kostenlosen OnWorks-Hosting-Provider über eine unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, Windows-Online-Emulator oder MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
victor - Versuche, Verifikationsbedingungen mit SMT-Solvern zu erfüllen
ZUSAMMENFASSUNG
Sieger [EINHEIT]
BESCHREIBUNG
Das Sieger Befehl ist ein Wrapper um ViCToR (vct), was die Verwendung vereinfacht. Sieger
übersetzt SPARK-Verifizierungsbedingungen in SMTlib und führt sie einem SMT-Solver zu.
SPARK wird mit einem solchen SMT-Solver geliefert, alter-ergo, aber es ist möglich, andere Solver zu verwenden
sowie cvc3.
Der beabsichtigte Zweck von victor besteht darin, echte VCs zu entladen, die vom Simplifier übrig geblieben sind, und nicht
Ersetzen Sie den Simplifier. Bitte beachten Sie auch, dass ViCToR als experimentell angesehen wird
Funktion im Moment.
Diese Handbuchseite fasst nur die Sieger Befehlszeilen-Flags finden Sie in der vollständigen
VictorWrapper-Handbuch für weitere Informationen.
OPTIONAL
Diese Optionen folgen nicht ganz der üblichen GNU-Befehlszeilensyntax, da Optionen mit beginnen
ein einzelner Strich statt der üblichen zwei.
-h, -Hilfe
Zeigt die Befehlszeilenhilfe an.
-t=SECONDS
Timeout des SMT-Solvers nach so vielen Sekunden (standardmäßig 5) mit unlimit. Nach
Zeitüberschreitung deaktivieren Geben Sie 0 an.
-m=MEGABYTE
Begrenzen Sie den SMT-Solver auf diese vielen MiB virtuellen Speichers (standardmäßig keine Begrenzung) mit
unlimit.
-v Ignorieren Sie das Vorhandensein von siv-Dateien und verarbeiten Sie nur vcg-Dateien. Standardmäßig angegeben
a EINHEIT wie foo, victor versucht zuerst, foo.siv zu verarbeiten und fällt dann zurück
zu foo.vcg.
-einfach Einfacher Modus – Unterdrücke Timings und Versionen.
-Löser=LÖSER
Gibt einen alternativen SMT-Solver an. Standardmäßig verwenden wir alt-ergo. Kann einer von alt-
ergo, cvc3, yices oder z3. Der Alt-Ergo-Solver wird mit SPARK ausgeliefert. Der cvc3
Solver ist Teil von Debian. Die yices- und z3-Solver sind proprietär.
Nutzen Sie victor online mit den onworks.net-Diensten
