module Eval_behaviors:sig
..end
Evaluate the assigns assigns
of kf
(for one or more behaviors)
in the state with_formals
.
per_behavior
indicates that the assigns clause is computed separately
for each behavior. It is used to control the emission of warnings.
val compute_using_specification : Kernel_function.t ->
Cil_types.funspec ->
call_kinstr:Cil_types.kinstr ->
with_formals:Cvalue.Model.t -> Value_types.call_result
kf
in state with_formals
, first by reducing by the
preconditions, then by evaluating the assigns, then by reducing
by the post-conditions.