Module Eval_behaviors

module Eval_behaviors: sig .. end
Evaluation of functions using their specification

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
Evaluate kf in state with_formals, first by reducing by the preconditions, then by evaluating the assigns, then by reducing by the post-conditions.