From 8a5fa8ed06036044e0d5b20d9eff3c6809862049 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 16 Sep 2021 16:15:14 +0200
Subject: [PATCH] Dummy initial printer.
---
config/drivers/pyrat.drv | 2 ++
nnet.opam | 5 ++---
src/dune | 2 ++
src/printer/pyrat.ml | 13 +++++++++++++
src/verification.ml | 13 +++++++------
tests/simple.t | 1 +
6 files changed, 27 insertions(+), 9 deletions(-)
create mode 100644 src/printer/pyrat.ml
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index 6c21b2b1..ec70c583 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -1,5 +1,7 @@
(* Why3 drivers for PyRAT *)
+prelude "(* this is the prelude for PyRAT *)"
+
(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
valid "^Inconsistent assumption$"
diff --git a/nnet.opam b/nnet.opam
index 4871796a..ea6f2c52 100644
--- a/nnet.opam
+++ b/nnet.opam
@@ -9,7 +9,7 @@ depends: [
"odoc" {with-doc}
]
build: [
- ["dune" "subst" "--root" "."] {dev}
+ ["dune" "subst"] {dev}
[
"dune"
"build"
@@ -17,8 +17,7 @@ build: [
name
"-j"
jobs
- "--promote-install-files"
- "false"
+ "--promote-install-files=false"
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
diff --git a/src/dune b/src/dune
index 3d9b62cc..a8874d6f 100644
--- a/src/dune
+++ b/src/dune
@@ -6,6 +6,8 @@
(package caisar)
)
+(copy_files printer/*)
+
(generate_sites_module
(module dirs)
(sites caisar))
diff --git a/src/printer/pyrat.ml b/src/printer/pyrat.ml
new file mode 100644
index 00000000..5ec59fe8
--- /dev/null
+++ b/src/printer/pyrat.ml
@@ -0,0 +1,13 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(**************************************************************************)
+
+let print_task args ?old:_ fmt _task =
+ let open Why3 in
+ Printer.print_prelude fmt args.Printer.prelude
+
+let () =
+ Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
+ print_task
diff --git a/src/verification.ml b/src/verification.ml
index 1fa65915..74d0fd55 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -6,6 +6,7 @@
open Base
module Format = Caml.Format
+module Filename = Caml.Filename
let () = Language.register ()
@@ -24,23 +25,23 @@ let verify format loadpath prover file =
match file with
| "-" ->
("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
- | filename ->
- let mlw_files, _ = Env.(read_file ?format base_language env filename) in
- (filename, mlw_files)
+ | file ->
+ let mlw_files, _ = Env.(read_file ?format base_language env file) in
+ (file, mlw_files)
in
Wstdlib.Mstr.iter
(fun _ theory ->
let tasks = Task.split_theory theory None None in
let prover =
- Whyconf.filter_one_prover config (Why3.Whyconf.mk_filter_prover prover)
+ Whyconf.(filter_one_prover config (mk_filter_prover prover))
in
let driver =
match String.chop_prefix ~prefix:"caisar_drivers/" prover.driver with
| None -> Whyconf.(load_driver (get_main config) env prover)
| Some file ->
let file =
- Caml.Filename.concat
- (Caml.Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
+ Filename.concat
+ (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
file
in
Driver.load_driver_absolute env file prover.extra_drivers
diff --git a/tests/simple.t b/tests/simple.t
index 9796780f..2f22cd59 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -46,6 +46,7 @@ Test verify
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.0, OK.
<autodetect>3 prover(s) added
+ (* this is the prelude for PyRAT *)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(* this is a prelude for Alt-Ergo real arithmetic *)
type string
--
GitLab