Frama-C:
Plug-ins:
Libraries:

Frama-C API - Loops

Loop specific actions.

Modify the given stmt loop to insert the code which verifies the loop annotations, ie. preserves its loop invariants and checks the loop variant. Also return the modified environment.

mk_nested_loops ~loc mk_innermost_block kf env lvars creates nested loops (with the proper statements for initializing the loop counters) from the list of logic variables lvars. Quantified variables create loops while let-bindings simply create new variables. The mk_innermost_block closure creates the statements of the innermost block.