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] Probably a solution for the Jessie Bug

  • Subject: [Frama-c-discuss] Probably a solution for the Jessie Bug
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Tue Nov 18 15:39:21 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