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] Memory locations

Hi Frama-C users,

I would like to come back on paragraph 2.3.4 page 24 of the ACSL 
preliminary design version 1.3 (the last one): in this paragraph there are 
quite a few ways of defining a set of memory locations, but I don't find 
any way of defining memory locations based on regular expressions. Doing 
this could be really useful.

For example, and in particular in code generated by Scade, we get pieces 
of code which look like (this example is based on a real piece of code I 
worked on) the following:

typedef struct{
  int i_1;
  int i_2;
  [...]
  int i_15;
  int o_1;
  [...]
  int o_9;
} type_1;

typedef struct{
  int i_1;
  [...]
  int i_17;
  int o_1;
  [...]
  int o_24;
} type_2;

void function_1(type_1* arg){
  arg->o_1=arg->i_1 - (arg->i_2 * arg->i_3);
  [...]
  // function_1 reads arg->i_1, ..., arg->i_15 and assigns arg->o_1, ..., 
arg->o_9
  // "i" is for "in", "o" is for "out"
}

void function_2(type_2* arg){
  arg->o_1=arg->i_1 + arg->i_2;
  [...]
  // function_2 reads arg->i_1, ..., arg->i_17 and assigns arg->o_1, ..., 
arg->o_24
}

typedef struct{
  int i_1;
  [...]
  int i_5;
  int o_1;
  [...]
  int o_7;
  type_1 s_1;
  type_2* s_2;
} type_3;

void function_3(type_3* arg){
  arg->o_1=arg->i_5;
  [...]
  function_1(&(arg->s_1));
  function_2(arg->s_2);
  // function_3 reads arg->i_1, ..., arg->i_5 and assigns arg->o_1, ..., 
arg->o_7
  // function_3 also calls function_1 and funtion_2 on s_1 and s_2 
respectively
}

Now, if I want to put the assigns annotations for this code, I would need 
to write something very very long like:

/*@ assigns arg->o_1, arg->o_2, [...], arg->o_9;   */
void function_1(type_1* arg);

/*@ assigns arg->o_1, arg->o_2, [...], arg->o_24;   */
void function_2(type_2* arg);

/*@ assigns arg->o_1, arg-> o_2, [...], arg->o_7,
  @                   arg->s_1.o_1, arg->s_1.o_2, [...], arg->s_1.o_9,
  @                   arg->s_2->o_1, arg->s_2->o_2, [...], arg->s_1->o_24;
  @*/
void function_3(type_3* arg);

In particular, this last annotation can be very very long (on one example, 
I get a 100-line long annotation doing that), and extremely painful to 
write. It would be much more convenient to be able to write something like 
(even if the star I am using here is traditional, it is probably not 
well-suited):

/*@ assigns arg->o_*;
   @*/
void function_1(type_1* arg);
/*@ assigns arg->o_*;
  @*/
void function_2(type_2* arg);
/*@ assigns arg->o_*,
  @                   arg->s_1.o_*,
  @                   arg->s_2->o_*;
  @*/
void function_3(type_3* arg);

or even something better (but meaning the same) like:

/*@ assigns arg->*o_*
  @*/
void function_3(type_3* arg);

I think this would be really neat and probably not too difficult to 
implement knowing the different structs involved. Also, in the above 
annotation on function_3, I would be curious to know the exact meaning, 
for ACSL and Frama-C of the following annotations (according to the 
current design):
- assigns arg                   // does it mean changes the address of 
arg, of just the o_* and the addresses of arg->s_1 and arg->s_2, or some 
other signification?
- assigns *arg                 // same question
- assigns arg->s_1        // same question
- assigns &(arg->s_1)  // same question
- assigns arg->s_2        // same question
- assigns *(arg->s_2)    // same question

What do you think about all this?

Thanks a lot for reading until now!

Jean-Baptiste Jeannin
#
" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."

 " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
#
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081029/c9747fc3/attachment.html