diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index 70fd2b157c38f435d12350a3f395d4cadee490ff..353dd6bb25ce5212eca677d3f7cc8f1651a48b07 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -911,7 +911,7 @@ module BuiltinsOverrides = Fall back to <f> if <ffc> cannot handle its arguments." let default = Kernel_function.Map.empty end) -let () = add_precision_dep BuiltinsOverrides.parameter +let () = add_correctness_dep BuiltinsOverrides.parameter (* Exported in Eva.mli. *) let use_builtin key name = @@ -987,7 +987,7 @@ module UsePrototype = let help = "Use the ACSL specification of the functions instead of \ their definitions" end) -let () = add_precision_dep UsePrototype.parameter +let () = add_correctness_dep UsePrototype.parameter let () = Parameter_customize.set_group precision_tuning module SkipLibcSpecs = @@ -1259,6 +1259,7 @@ module AllocReturnsNull= let help = "Memory allocation built-ins (malloc, calloc, realloc) are \ modeled as nondeterministically returning a null pointer" end) +let () = add_correctness_dep AllocReturnsNull.parameter let () = Parameter_customize.set_group malloc module MallocLevel = @@ -1271,6 +1272,7 @@ module MallocLevel = besides the initial one, for each callstack (defaults to 0)" end) let () = MallocLevel.set_range 0 max_int +let () = add_precision_dep MallocLevel.parameter (* -------------------------------------------------------------------------- *) (* --- Deprecated aliases --- *)