Skip to content
Snippets Groups Projects
Commit 2e05a770 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Fixes correctness and precision dependencies for some Eva parameters.

parent 74eabf81
No related branches found
No related tags found
No related merge requests found
...@@ -911,7 +911,7 @@ module BuiltinsOverrides = ...@@ -911,7 +911,7 @@ module BuiltinsOverrides =
Fall back to <f> if <ffc> cannot handle its arguments." Fall back to <f> if <ffc> cannot handle its arguments."
let default = Kernel_function.Map.empty let default = Kernel_function.Map.empty
end) end)
let () = add_precision_dep BuiltinsOverrides.parameter let () = add_correctness_dep BuiltinsOverrides.parameter
(* Exported in Eva.mli. *) (* Exported in Eva.mli. *)
let use_builtin key name = let use_builtin key name =
...@@ -987,7 +987,7 @@ module UsePrototype = ...@@ -987,7 +987,7 @@ module UsePrototype =
let help = "Use the ACSL specification of the functions instead of \ let help = "Use the ACSL specification of the functions instead of \
their definitions" their definitions"
end) end)
let () = add_precision_dep UsePrototype.parameter let () = add_correctness_dep UsePrototype.parameter
let () = Parameter_customize.set_group precision_tuning let () = Parameter_customize.set_group precision_tuning
module SkipLibcSpecs = module SkipLibcSpecs =
...@@ -1259,6 +1259,7 @@ module AllocReturnsNull= ...@@ -1259,6 +1259,7 @@ module AllocReturnsNull=
let help = "Memory allocation built-ins (malloc, calloc, realloc) are \ let help = "Memory allocation built-ins (malloc, calloc, realloc) are \
modeled as nondeterministically returning a null pointer" modeled as nondeterministically returning a null pointer"
end) end)
let () = add_correctness_dep AllocReturnsNull.parameter
let () = Parameter_customize.set_group malloc let () = Parameter_customize.set_group malloc
module MallocLevel = module MallocLevel =
...@@ -1271,6 +1272,7 @@ module MallocLevel = ...@@ -1271,6 +1272,7 @@ module MallocLevel =
besides the initial one, for each callstack (defaults to 0)" besides the initial one, for each callstack (defaults to 0)"
end) end)
let () = MallocLevel.set_range 0 max_int let () = MallocLevel.set_range 0 max_int
let () = add_precision_dep MallocLevel.parameter
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* --- Deprecated aliases --- *) (* --- Deprecated aliases --- *)
......
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