Frama-C API - Interlang_trans
The compilation of E-ACSL to Cil currently has two different compilation schemes, the original direct-to-Cil compilation scheme, and the new compilation scheme, in which E-ACSL is first translated into an intermediate language Interlang and only then into Cil. The implementation of the new compilation scheme is not yet complete and will fail on many E-ACSL expressions. Therefore we supply in this module a function that tries first the new compilation schemes and only in case of failure applies the older one.
type 'a il_compiler = 'a -> Interlang.exp Interlang_gen.ma compiler that translates E-ACSL predicates to an expression of the E-ACSL intermediate language (see Interlang) using the Interlang_gen.m monad.
type 'a compiler = loc:Frama_c_kernel.Cil_types.location -> adata:Assert.t -> env:Env.t -> kf:Frama_c_kernel.Cil_types.kernel_function -> 'a -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.ta direct-to-Cil compiler that compiles E-ACSL predicates directly to Cil.
val try_il_compiler : 'a il_compiler -> 'a compiler -> 'a compilercompile a predicate to a Cil expression by first trying the new compilation scheme via the E-ACSL intermediate language (see Interlang); if that fails raising Interlang_gen.Not_covered, fall back to the old direct-to-Cil compilation scheme.