Skip to main content

never_errors_asserts

cedar_policy_symcc

Function never_errors_asserts 

Source 
pub fn never_errors_asserts<'a>(
    policy: &'a CompiledPolicy,
) -> WellFormedAsserts<'a>
Expand description

Generate the WellFormedAsserts for the check_never_errors() operation, without actually calling a solver.

That is, the result of

compiler.check_unsat(never_errors_asserts(policy))

should be the same as compiler.check_never_errors_opt(policy).

Likewise, the result of

compiler.check_sat(never_errors_asserts(policy))

should be the same as compiler.check_never_errors_with_counterexample_opt(policy).

NOTE: This API is an experimental feature, and the API may change or break in the future.