From 119b786d9039d6c500d485522c47d078cb03ea9f Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 25 Oct 2023 10:56:52 +0200
Subject: [PATCH] [cmdline] Provide a short version for the define constant
option.
---
CHANGES.md | 4 ++--
src/main.ml | 4 ++--
tests/define.t | 16 ++++++++--------
3 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index 8ef6907..736ba5e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,7 @@
## Unreleased
-- Add --define (or --def) to define the value of a declared constant from
- the command line.
+- Add command line option --define (or -D) to define the value of a declared
+ constant in any specification file to verify.
# 0.2.1 (19-09-2023)
diff --git a/src/main.ml b/src/main.ml
index f41eb63..29663b7 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -261,8 +261,8 @@ let verify_cmd =
let doc = "Define a declared constant with the given value." in
Arg.(
value
- & opt_all (Arg.pair ~sep:':' string string) []
- & info [ "define"; "def" ] ~doc ~docv:"name:value")
+ & opt_all (pair ~sep:':' string string) []
+ & info [ "D"; "define" ] ~doc ~docv:"name:value")
in
let files =
let doc = "File(s) to verify." in
diff --git a/tests/define.t b/tests/define.t
index 058ca5b..0da98bd 100644
--- a/tests/define.t
+++ b/tests/define.t
@@ -14,13 +14,13 @@ Test interpretation of on-the-fly definition of toplevel constants
> end
> EOF
- $ caisar verify --prover PyRAT file.mlw --def n:1 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -D n:1 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
[DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
true
[ERROR] Invalid argument: No neural network model found in task
- $ caisar verify --prover PyRAT file.mlw --def n:2 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -Dn:2 2>&1 | ./filter_tmpdir.sh
[ERROR] Invalid argument: No neural network model found in task
$ cat > file.mlw <<EOF
@@ -33,13 +33,13 @@ Test interpretation of on-the-fly definition of toplevel constants
> end
> EOF
- $ caisar verify --prover PyRAT file.mlw --def n:foo --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -D n:foo --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
[DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
true
[ERROR] Invalid argument: No neural network model found in task
- $ caisar verify --prover PyRAT file.mlw --def n:bar 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -D n:bar 2>&1 | ./filter_tmpdir.sh
[ERROR] Invalid argument: No neural network model found in task
$ cat > file.mlw <<EOF
@@ -50,13 +50,13 @@ Test interpretation of on-the-fly definition of toplevel constants
> end
> EOF
- $ caisar verify --prover PyRAT file.mlw --def n:1.0 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -D n:1.0 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
[DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
true
[ERROR] Invalid argument: No neural network model found in task
- $ caisar verify --prover PyRAT file.mlw --def n:foo 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -D n:foo 2>&1 | ./filter_tmpdir.sh
[ERROR] 'n' expects a numerical constant, got 'foo' instead
$ cat > file.mlw <<EOF
@@ -67,11 +67,11 @@ Test interpretation of on-the-fly definition of toplevel constants
> end
> EOF
- $ caisar verify --prover PyRAT file.mlw --def n:true --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -D n:true --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
[DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
true
[ERROR] Invalid argument: No neural network model found in task
- $ caisar verify --prover PyRAT file.mlw --def n:false 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT file.mlw -D n:false 2>&1 | ./filter_tmpdir.sh
[ERROR] Invalid argument: No neural network model found in task
--
GitLab