Skip to content
Snippets Groups Projects
Commit fa9e9694 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by Thibault Martin
Browse files

[kernel] add a test for Parameter_sig.Decimal

parent 5d747cbf
No related branches found
No related tags found
No related merge requests found
/* 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 */
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
[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
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
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]]")
{
"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
[test] User Error: argument of -test-decimal-option must be at least 0.000000.
[kernel] Plug-in test aborted: invalid user input.
[test] User Error: argument of -test-decimal-option must be no more than 1.000000.
[kernel] Plug-in test aborted: invalid user input.
[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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment