Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using frama-c script to get proof obligations

  • Subject: [Frama-c-discuss] Using frama-c script to get proof obligations
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Thu, 19 Jun 2014 18:11:49 +0200
  • In-reply-to: <CAM1QBJNHX1_xp=tUw+EMim1Lu78g13z6E9azqJpbQYQKcLNHFw@mail.gmail.com>
  • References: <CAM1QBJONYOzVxGpeid81KJ_YVnbAzWpcQ5b206eMuH31OPOOZA@mail.gmail.com> <D8D4FC26B114714EB1FAE173346799BB22FAE2E2@EXDAG0-A1.intra.cea.fr> <CAM1QBJNHX1_xp=tUw+EMim1Lu78g13z6E9azqJpbQYQKcLNHFw@mail.gmail.com>
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