--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2014 ---
Le 15.05.2014 13:09, Lo?c Correnson a ?crit?: > It is also my guess. Have also a look to frama-c -print-*-path > options, -share and -wp-share options. Everything seems normal about the path but since I found a workaround it's hard to test it now. > Of course, this is the nature of inductive types, indeed. > You should also consider the following methodology : > > 1. Declare in Coq your inductive predicate, in a self-consistent Coq > module. > > 2. Declare an *abstract* predicate in ACSL, and state the useful > lemmas you want to USE for proving your code. > > 3. Define a WP-driver (WP ? 2.3.10) that informs WP to link the ACSL > predicate to your Coq module. > > And then, your done in a very sound way. > This can be generalized for types and many other interesting things. This seems to be an interesting methodology, that offers a lot of possibilities. Thanks for yours answers. Guillaume Davy