diff --git a/tests/misc/decimal_parameter.i b/tests/misc/decimal_parameter.i
new file mode 100644
index 0000000000000000000000000000000000000000..60ca169428245e032256737a2090ac5cf75b49fd
--- /dev/null
+++ b/tests/misc/decimal_parameter.i
@@ -0,0 +1,14 @@
+/* run.config*
+ PLUGIN: @EVA_PLUGINS@
+ MODULE: @PTEST_NAME@
+ OPT: -test-decimal-option 0.12 -test-deprecated-option 0.12
+ OPT: -autocomplete test
+ OPT: -test-h
+ OPT: -print-config-json
+ EXIT: 1
+ OPT: -test-decimal-option -1.0
+ OPT: -test-decimal-option 2.0
+ OPT: -test-decimal-option x
+*/
+
+/* Just build and run the module */
diff --git a/tests/misc/decimal_parameter.ml b/tests/misc/decimal_parameter.ml
new file mode 100644
index 0000000000000000000000000000000000000000..32625056355b1c8ece747058a0d367af54034683
--- /dev/null
+++ b/tests/misc/decimal_parameter.ml
@@ -0,0 +1,36 @@
+let plugin_name = "test"
+
+include Plugin.Register (struct
+ let name = plugin_name
+ let shortname = name
+ let help = "A fake plugin for test purpose"
+ end)
+
+module TestDecimal = Decimal (struct
+ let option_name = "-test-decimal-option"
+ let help = "test option"
+ let arg_name = "x"
+ let default = 0.0
+ end)
+
+let () =
+ TestDecimal.set_range ~min:0.0 ~max:1.0;
+ TestDecimal.add_aliases ~deprecated:true
+ ["-test-deprecated-option"]
+
+module TestDecimalDefaultRange = Decimal (struct
+ let option_name = "-test-default-range"
+ let help = "test option"
+ let arg_name = "x"
+ let default = 0.0
+ end)
+
+
+
+let run_test () =
+ let _range = TestDecimal.get_range () in
+ let _range = TestDecimalDefaultRange.get_range () in
+ feedback "-test-decimal-option set to %f" (TestDecimal.get ())
+
+let () =
+ Boot.Main.extend run_test
diff --git a/tests/misc/oracle/decimal_parameter.0.res.oracle b/tests/misc/oracle/decimal_parameter.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ef2d04e2e69f7c107bab040465f85459c2a6fcf9
--- /dev/null
+++ b/tests/misc/oracle/decimal_parameter.0.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Warning: -test-deprecated-option is a deprecated alias
+ for option -test-decimal-option. Please use -test-decimal-option instead.
+[kernel] Parsing decimal_parameter.i (no preprocessing)
+[test] -test-decimal-option set to 0.120000
diff --git a/tests/misc/oracle/decimal_parameter.1.res.oracle b/tests/misc/oracle/decimal_parameter.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5d4b118bcdc3baf74921a26bc5acffb1d29248ca
--- /dev/null
+++ b/tests/misc/oracle/decimal_parameter.1.res.oracle
@@ -0,0 +1,11 @@
+Plugin: test
+ -test-debug: int (0, 4611686018427387903)
+ -test-decimal-option: float (0.000000, 1.000000)
+ -test-default-range: float
+ -test-help: bool
+ -test-log: string
+ -test-msg-key: string
+ -test-session: string
+ -test-share: string
+ -test-verbose: int (0, 4611686018427387903)
+ -test-warn-key: string
diff --git a/tests/misc/oracle/decimal_parameter.2.res.oracle b/tests/misc/oracle/decimal_parameter.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bee1eb870b2aa46f5a86ab1a32df81f686ef5157
--- /dev/null
+++ b/tests/misc/oracle/decimal_parameter.2.res.oracle
@@ -0,0 +1,48 @@
+Plug-in name: test
+Plug-in shortname: test
+Description: A fake plugin for test purpose
+
+Most options of the form '-test-option-name' and without any parameter
+have an opposite with the name '-test-no-option-name'.
+
+Most options of the form '-option-name' and without any parameter
+have an opposite with the name '-no-option-name'.
+
+Options taking a string as argument should preferably be written
+-option-name="argument".
+
+***** LIST OF AVAILABLE OPTIONS:
+
+-test-decimal-option <x> test option
+-test-deprecated-option <x> alias for option -test-decimal-option
+-test-default-range <x> test option
+
+*** GETTING INFORMATION
+
+-test-help help of plug-in test
+-test-h alias for option -test-help
+
+*** OUTPUT MESSAGES
+
+-test-debug <n> level of debug for plug-in test (default to 0)
+-test-log <K_1:file_1,...> copy log messages from test to a file. <K> is a
+ combination of these characters:
+ a: ALL messages (equivalent to 'dfiruw')
+ d: debug e: user or internal error (same as 'iu')
+ f: feedback i: internal error
+ r: result u: user error w: warning
+ An empty <K> (e.g. ":file.txt") defaults to 'iruw'. One
+ plug-in can output to several files and vice-versa.
+ (preferably use -test-log="K_1:file_1,...")
+-test-msg-key <k1[,...,kn]> enables message display for categories
+ <k1>,...,<kn>. Use -test-msg-key help to get a list of
+ available categories, and * to enable all categories
+ (preferably use -test-msg-key="k1[,...,kn]")
+-test-verbose <n> level of verbosity for plug-in test (default to 1)
+-test-warn-key <k1[=s1][,...,kn[=sn]]> set warning status for category <k1>
+ to <s1>,...,<kn> to <sn>. Use -test-warn-key help to get
+ a list of available categories, and * to enable all
+ categories. Possible statuses are inactive,
+ feedback-once, once, active, error-once, error, and
+ abort. Defaults to active (preferably use
+ -test-warn-key="k1[=s1][,...,kn[=sn]]")
diff --git a/tests/misc/oracle/decimal_parameter.3.res.oracle b/tests/misc/oracle/decimal_parameter.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6ff7a3a4a89d187bcd811682176e35262d8cedee
--- /dev/null
+++ b/tests/misc/oracle/decimal_parameter.3.res.oracle
@@ -0,0 +1,354 @@
+{
+ "codename": "Zinc",
+ "current_machdep": "x86_64",
+ "datadir": "/home/perrelle/work/frama-c-clones/ml4eva/_build/install/default/share/frama-c/share",
+ "datadirs": [
+ "/home/perrelle/work/frama-c-clones/ml4eva/_build/install/default/share/frama-c/share"
+ ],
+ "framac_libc": "/home/perrelle/work/frama-c-clones/ml4eva/_build/install/default/share/frama-c/share/libc",
+ "is_gui": false,
+ "lib_dir": "/home/perrelle/work/frama-c-clones/ml4eva/_build/install/default/lib/frama-c/lib",
+ "lib_dirs": [
+ "/home/perrelle/work/frama-c-clones/ml4eva/_build/install/default/lib/frama-c/lib"
+ ],
+ "machdeps": [
+ "x86_64", "ppc_32", "gcc_x86_16", "x86_32", "gcc_x86_64", "gcc_x86_32",
+ "msvc_x86_64", "avr_8", "avr_16", "x86_16"
+ ],
+ "major_version": 30,
+ "minor_version": 0,
+ "parameters": {
+ "--help": false,
+ "--list-plugins": false,
+ "-absolute-valid-range": "",
+ "-access-path": false,
+ "-add-symbolic-path": "",
+ "-aggressive-merging": false,
+ "-allow-duplication": true,
+ "-annot": true,
+ "-asm-contracts": true,
+ "-asm-contracts-auto-validate": false,
+ "-asm-contracts-ensure-init": false,
+ "-ast-diff": false,
+ "-audit-check": "<unknown location>",
+ "-audit-prepare": "<unknown location>",
+ "-autocomplete": "",
+ "-autoload-plugins": false,
+ "-big-ints-hex": -1,
+ "-c11": false,
+ "-cache": "<unknown location>",
+ "-cache-size": 2,
+ "-calldeps": false,
+ "-calldeps-print": true,
+ "-cg": "<unknown location>",
+ "-cg-debug": 0,
+ "-cg-function-pointers": true,
+ "-cg-help": false,
+ "-cg-log": "",
+ "-cg-msg-key": "",
+ "-cg-roots": "",
+ "-cg-service-roots": "",
+ "-cg-services": true,
+ "-cg-session": "<unknown location>",
+ "-cg-share": "<unknown location>",
+ "-cg-uncalled": true,
+ "-cg-uncalled-leaf": false,
+ "-cg-verbose": 1,
+ "-cg-warn-key": "",
+ "-check": false,
+ "-codpds": false,
+ "-collapse-call-cast": true,
+ "-config": "<unknown location>",
+ "-constfold": false,
+ "-copy": false,
+ "-cpp-command": "",
+ "-cpp-extra-args": "",
+ "-cpp-extra-args-per-file": "",
+ "-cpp-frama-c-compliant": true,
+ "-debug": 0,
+ "-deps": false,
+ "-deps-print": true,
+ "-deref": false,
+ "-deterministic": true,
+ "-dump-dependencies": "",
+ "-eager-load-sources": false,
+ "-enums": "gcc-enums",
+ "-eva": false,
+ "-eva-all-rounding-modes-constants": false,
+ "-eva-alloc-builtin": "by_stack",
+ "-eva-alloc-functions": "calloc,malloc,realloc",
+ "-eva-alloc-returns-null": true,
+ "-eva-annot": "",
+ "-eva-auto-loop-unroll": 0,
+ "-eva-bitwise-domain": false,
+ "-eva-builtin": "",
+ "-eva-builtins-auto": true,
+ "-eva-builtins-list": false,
+ "-eva-context-depth": 2,
+ "-eva-context-valid-pointers": false,
+ "-eva-context-width": 2,
+ "-eva-cvalue-domain": true,
+ "-eva-debug": 0,
+ "-eva-default-loop-unroll": 100,
+ "-eva-descending-iteration": "no",
+ "-eva-domains": "cvalue",
+ "-eva-domains-function": "",
+ "-eva-enumerate-cond": true,
+ "-eva-equality-domain": false,
+ "-eva-equality-through-calls": "formals",
+ "-eva-equality-through-calls-function": "",
+ "-eva-flamegraph": "<unknown location>",
+ "-eva-force-print-summary": false,
+ "-eva-gauges-domain": false,
+ "-eva-help": false,
+ "-eva-hierarchical-convergence": false,
+ "-eva-ignore-recursive-calls": false,
+ "-eva-ilevel": 8,
+ "-eva-initialization-padding-globals": "yes",
+ "-eva-initialized-locals": false,
+ "-eva-inout-domain": false,
+ "-eva-interpreter-mode": false,
+ "-eva-interprocedural-history": false,
+ "-eva-interprocedural-splits": false,
+ "-eva-join-results": true,
+ "-eva-log": "",
+ "-eva-memexec": true,
+ "-eva-min-loop-unroll": 0,
+ "-eva-mlevel": 0,
+ "-eva-msg-key": "",
+ "-eva-multidim-disjunctive-invariants": false,
+ "-eva-multidim-domain": false,
+ "-eva-multidim-fast-imprecise": false,
+ "-eva-multidim-segment-limit": 8,
+ "-eva-new-initial-state": 0,
+ "-eva-no-results-domain": "",
+ "-eva-no-results-function": "",
+ "-eva-numerors-interaction": "both",
+ "-eva-numerors-log-file": "<unknown location>",
+ "-eva-numerors-real-size": 128,
+ "-eva-octagon-domain": false,
+ "-eva-octagon-through-calls": false,
+ "-eva-oracle-depth": 2,
+ "-eva-partition-history": 0,
+ "-eva-partition-value": "",
+ "-eva-plevel": 200,
+ "-eva-precision": -1,
+ "-eva-print": true,
+ "-eva-print-callstacks": false,
+ "-eva-printer-domain": false,
+ "-eva-reduce-on-logic-alarms": false,
+ "-eva-reduction-depth": 4,
+ "-eva-remove-redundant-alarms": true,
+ "-eva-report-red-statuses": "<unknown location>",
+ "-eva-results": true,
+ "-eva-session": "<unknown location>",
+ "-eva-share": "<unknown location>",
+ "-eva-show-perf": false,
+ "-eva-show-progress": false,
+ "-eva-show-slevel": 100,
+ "-eva-sign-domain": false,
+ "-eva-skip-stdlib-specs": true,
+ "-eva-slevel": 0,
+ "-eva-slevel-function": "",
+ "-eva-slevel-merge-after-loop": "",
+ "-eva-split-limit": 100,
+ "-eva-split-return": "",
+ "-eva-split-return-function": "",
+ "-eva-statistics-file": "<unknown location>",
+ "-eva-stop-at-nth-alarm": 4611686018427387903,
+ "-eva-subdivide-non-linear": 0,
+ "-eva-subdivide-non-linear-function": "",
+ "-eva-symbolic-locations-domain": false,
+ "-eva-taint-domain": false,
+ "-eva-traces-domain": false,
+ "-eva-traces-dot": "<unknown location>",
+ "-eva-traces-project": false,
+ "-eva-traces-unify-loop": false,
+ "-eva-traces-unroll-loop": true,
+ "-eva-undefined-pointer-comparison-propagate-all": false,
+ "-eva-unroll-recursive-calls": 0,
+ "-eva-use-spec": "",
+ "-eva-verbose": 1,
+ "-eva-warn-copy-indeterminate": "",
+ "-eva-warn-key": "",
+ "-eva-warn-pointer-subtraction": true,
+ "-eva-warn-signed-converted-downcast": false,
+ "-eva-warn-undefined-pointer-comparison": "pointer",
+ "-eva-widening-delay": 3,
+ "-eva-widening-period": 2,
+ "-explain": false,
+ "-fct-pdg": "",
+ "-float-hex": false,
+ "-float-normal": false,
+ "-float-relative": false,
+ "-frama-c-stdlib": true,
+ "-from-debug": 0,
+ "-from-help": false,
+ "-from-log": "",
+ "-from-msg-key": "",
+ "-from-session": "<unknown location>",
+ "-from-share": "<unknown location>",
+ "-from-verbose": 1,
+ "-from-verify-assigns": false,
+ "-from-warn-key": "",
+ "-generated-spec-custom": "",
+ "-generated-spec-mode": "frama-c",
+ "-initialized-padding-locals": true,
+ "-inline-calls": "",
+ "-inline-stmt-contracts": false,
+ "-inout": false,
+ "-inout-debug": 0,
+ "-inout-help": false,
+ "-inout-log": "",
+ "-inout-msg-key": "",
+ "-inout-print": true,
+ "-inout-session": "<unknown location>",
+ "-inout-share": "<unknown location>",
+ "-inout-verbose": 1,
+ "-inout-warn-key": "",
+ "-inout-with-formals": false,
+ "-input": false,
+ "-input-with-formals": false,
+ "-json-compilation-database": "<unknown location>",
+ "-keep-comments": false,
+ "-keep-logical-operators": false,
+ "-keep-switch": false,
+ "-keep-unused-functions": "specified",
+ "-keep-unused-types": false,
+ "-kernel-debug": 0,
+ "-kernel-help": false,
+ "-kernel-log": "",
+ "-kernel-msg-key": "",
+ "-kernel-share": "<unknown location>",
+ "-kernel-verbose": 1,
+ "-kernel-warn-key": "",
+ "-lib-entry": false,
+ "-load": "<unknown location>",
+ "-load-library": "",
+ "-load-module": "@default,decimal_parameter.cmxs",
+ "-load-plugin": "@default,from,inout,eva,scope,variadic",
+ "-machdep": "x86_64",
+ "-main": "main",
+ "-memory-footprint": 6,
+ "-ocode": "<unknown location>",
+ "-orig-name": false,
+ "-out": false,
+ "-out-external": false,
+ "-pdg": false,
+ "-pdg-debug": 0,
+ "-pdg-dot": "",
+ "-pdg-help": false,
+ "-pdg-log": "",
+ "-pdg-msg-key": "",
+ "-pdg-print": false,
+ "-pdg-session": "<unknown location>",
+ "-pdg-share": "<unknown location>",
+ "-pdg-verbose": 1,
+ "-pdg-warn-key": "",
+ "-permissive": false,
+ "-pp-annot": false,
+ "-print": false,
+ "-print-as-is": false,
+ "-print-config": false,
+ "-print-config-json": true,
+ "-print-cpp-commands": false,
+ "-print-lib-path": false,
+ "-print-libc": false,
+ "-print-machdep": false,
+ "-print-machdep-header": false,
+ "-print-plugin-path": false,
+ "-print-return": false,
+ "-print-share-path": false,
+ "-print-version": false,
+ "-quiet": false,
+ "-remove-exn": false,
+ "-remove-inlined": "",
+ "-remove-projects": "",
+ "-safe-arrays": true,
+ "-save": "<unknown location>",
+ "-scope-debug": 0,
+ "-scope-defs-interproc": true,
+ "-scope-help": false,
+ "-scope-log": "",
+ "-scope-msg-key": "",
+ "-scope-session": "<unknown location>",
+ "-scope-share": "<unknown location>",
+ "-scope-verbose": 1,
+ "-scope-warn-key": "",
+ "-server-auto-log": false,
+ "-server-batch": "",
+ "-server-batch-output-dir": "",
+ "-server-debug": 0,
+ "-server-doc": "<unknown location>",
+ "-server-help": false,
+ "-server-log": "",
+ "-server-msg-key": "",
+ "-server-polling": 50,
+ "-server-session": "<unknown location>",
+ "-server-share": "<unknown location>",
+ "-server-socket": "",
+ "-server-socket-size": 256,
+ "-server-verbose": 1,
+ "-server-warn-key": "",
+ "-session": "<unknown location>",
+ "-set-project-as-default": false,
+ "-show-indirect-deps": false,
+ "-simplify-cfg": false,
+ "-simplify-trivial-loops": true,
+ "-state": "<unknown location>",
+ "-test-debug": 0,
+ "-test-decimal-option": 0.0,
+ "-test-default-range": 0.0,
+ "-test-help": false,
+ "-test-log": "",
+ "-test-msg-key": "",
+ "-test-session": "<unknown location>",
+ "-test-share": "<unknown location>",
+ "-test-verbose": 1,
+ "-test-warn-key": "",
+ "-time": "",
+ "-tty": true,
+ "-typecheck": true,
+ "-ulevel": 0,
+ "-ulevel-force": false,
+ "-unicode": true,
+ "-unspecified-access": false,
+ "-variadic-debug": 0,
+ "-variadic-help": false,
+ "-variadic-log": "",
+ "-variadic-msg-key": "",
+ "-variadic-session": "<unknown location>",
+ "-variadic-share": "<unknown location>",
+ "-variadic-strict": true,
+ "-variadic-translation": true,
+ "-variadic-verbose": 1,
+ "-variadic-warn-key": "",
+ "-verbose": 1,
+ "-version": false,
+ "-warn-invalid-bool": true,
+ "-warn-invalid-pointer": false,
+ "-warn-left-shift-negative": true,
+ "-warn-pointer-downcast": true,
+ "-warn-right-shift-negative": false,
+ "-warn-signed-downcast": false,
+ "-warn-signed-overflow": true,
+ "-warn-special-float": "non-finite",
+ "-warn-unsigned-downcast": false,
+ "-warn-unsigned-overflow": false,
+ "Input C files": ""
+ },
+ "plugin_dir": [
+ "/home/perrelle/work/frama-c-clones/ml4eva/_build/install/default/lib/frama-c/plugins"
+ ],
+ "plugins": [
+ "test", "scope", "pdg", "inout", "from analysis", "callgraph",
+ "Variadic", "Server", "Eva", "kernel"
+ ],
+ "preprocessor": "gcc -E -C -I.",
+ "preprocessor_is_gnu_like": true,
+ "preprocessor_keep_comments": true,
+ "preprocessor_supported_arch_options": [ "-m16", "-m32", "-m64" ],
+ "using_default_cpp": true,
+ "version": "30.0+dev",
+ "version_and_codename": "30.0+dev (Zinc)"
+}
\ No newline at end of file
diff --git a/tests/misc/oracle/decimal_parameter.4.res.oracle b/tests/misc/oracle/decimal_parameter.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..72aa00408cce6ec4baa65ec65681d88bd4648c1a
--- /dev/null
+++ b/tests/misc/oracle/decimal_parameter.4.res.oracle
@@ -0,0 +1,2 @@
+[test] User Error: argument of -test-decimal-option must be at least 0.000000.
+[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/decimal_parameter.5.res.oracle b/tests/misc/oracle/decimal_parameter.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..914fe929b4979863a96c23e17525f847cec9ea6a
--- /dev/null
+++ b/tests/misc/oracle/decimal_parameter.5.res.oracle
@@ -0,0 +1,2 @@
+[test] User Error: argument of -test-decimal-option must be no more than 1.000000.
+[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/decimal_parameter.6.res.oracle b/tests/misc/oracle/decimal_parameter.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2573d10b4115577af578a52476c1f2072cbd8c3e
--- /dev/null
+++ b/tests/misc/oracle/decimal_parameter.6.res.oracle
@@ -0,0 +1,3 @@
+[kernel] User Error: option `-test-decimal-option' requires a decimal number as argument.
+ use `frama-c -help' for more information.
+[kernel] Frama-C aborted: invalid user input.