package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct