--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on June 2014 ---
Hello, On 06/11/2014 06:48 PM, Jos? Pinheiro wrote: > I had already come to the same conclusion, but still thank you for the > clear answer. The folds you talk about are fold_requires, fold_assumes, > fold_ensures right? Right. For example fold_requires, i am having a bit > difficult understanding the type: > > val fold_requires :|(Emitter.t ->Cil_types.identified_predicate <./Cil_types.html#TYPEidentified_predicate> -> 'a -> 'a) -> > > Cil_types.kernel_function <./Cil_types.html#TYPEkernel_function> -> string -> 'a -> 'a| > > > I understand the Emmitter.t, Cil_types.identified_predicate, ('a -> 'a) > (fold accumulator) and kernel_function are to use inside the fold, but > what is the string? Stopage case? The string is the name of the behavior which the requires is defined in. If the user does not specify any behavior, it is part of the default behavior and then you can use Cil.default_behavior_name to get its name. > More, inside the fold_requires i intend the use module Property and its > smart constructors to build the identified property lists, but most of > them require Cil_types.kinstr , what is this type? From what i found > searching the api the only way to get it is to use the module CilE with > the function current_stmt, is this correct? CilE is useless here. Cil_types.kinstr is (an approximation of) a position in the source code, that is either a stmt (constructor Kstmt) or another point (constructor Kglobal) if there is no corresponding statement (e.g. for a function contract or a global annotation). Hope this helps, Julien