--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Probably a solution for the Jessie Bug



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