--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on November 2008 ---
Hi everyone! I think I found the answer to my question. In the last week, I sent an email, explaining that I?m not able to compile a file with axiomatic definitions as the following: /*@ axiomatic Predicate1a { @ predicate pred1{L1,L2}(int k1,int a1[],int b1[], int k2,int a2[],int b2[], int n); @ axiom pred1_start{L} : @ \forall int k1, int k2,int a[],int b[], @ int n, int i; @ k1==k2 ==> pred1{L,L}(k1,a,b,k2,a,b,n); @ axiom pred1_inv{L1,L2,L3} : @ \forall int k1,int a1[],int b1[], @ int k2,int a2[],int b2[], @ int k3,int a3[],int b3[], @ int n; @ pred1{L1,L2}(k1,a1,b1,k2,a2,b2,n) @ ==> k3 == k2 + 1 @ ==> \at(b3[k2],L3) == \at(a3[k2],L3) + 1 @ ==> (\forall int l; 0<=l<n ==> \at(a3[l],L3)== \at(a2[l],L2)) @ ==> (\forall int l; 0<=l<n && k2!=l ==> \at(b3[l],L3)== \at(b2[l],L2)) @ ==> pred1{L1,L3}(k1,a1,b1,k3,b3,b3,n); @ } @*/ But instead of writing axiomatic in this way, I specify axiomatic definition as the following definition: /*@ axiomatic Predicate1a { @ predicate pred1{L1,L2}(int k1,int a1[],int b1[], int k2,int a2[],int b2[], int n); @ } @ axiomatic Predicate1b { @ axiom pred1_start{L} : @ \forall int k1, int k2,int a[],int b[], @ int n, int i; @ k1==k2 ==> pred1{L,L}(k1,a,b,k2,a,b,n); @ axiom pred1_inv{L1,L2,L3} : @ \forall int k1,int a1[],int b1[], @ int k2,int a2[],int b2[], @ int k3,int a3[],int b3[], @ int n; @ pred1{L1,L2}(k1,a1,b1,k2,a2,b2,n) @ ==> k3 == k2 + 1 @ ==> \at(b3[k2],L3) == \at(a3[k2],L3) + 1 @ ==> (\forall int l; 0<=l<n ==> \at(a3[l],L3)== \at(a2[l],L2)) @ ==> (\forall int l; 0<=l<n && k2!=l ==> \at(b3[l],L3)== \at(b2[l],L2)) @ ==> pred1{L1,L3}(k1,a1,b1,k3,b3,b3,n); @ } @*/ Is not presented any error during the compilation process with the command: frama-c -jessie-analysis -jessie-gui -jc-opt -separation short_file.c and the proof obligations are generated. I?m sending this email, because I want to know if the solution I found is correct and generates the correct proof obligations. I?m sending the code as an attachment. Thanks for everything. Best regards, B?rbara -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081118/3bd263af/attachment-0001.html