Module E_ACSL.Translate_terms

to_exp ~adata ?inplace kf env t converts an ACSL term into a corresponding C expression.

• adata: assertion context.
• inplace: if the root term has a label, indicates if it should be immediately translated or if Translate_ats should be used to retrieve the translation.
• kf: The enclosing function.
• env: The current environment.
• t: The term to translate.

a version of to_exp that translates ACSL terms to the intermediate language instead to Cil.

denominator_zero_guard ~loc ~ctx ~adata ~kf ~env ~name ?root denom converts the ACSL term denom, representing the denominator of a division or modulo, into a corresponding expression using to_exp and a guard statement checking that denom != 0.

• loc: location used for the assertion.
• ctx: context used to create the zero term of the guard statement.
• adata: assertion context.
• kf: enclosing function.
• env: current environment.
• name: used for temporary variable names.
• root: root term containing the original division or modulo.
• denom: the term to translate.

Exceptin raised if untyped_to_exp would generate new statements in the environment

Convert an untyped ACSL term into a corresponding C expression.