Search code examples
pointersframa-carrays

How do you declare 'assigns' clause with multidimensional arrays in frama-c?

I have the following variables:

int** send_count;
message_struct*** send_queue;

And I have a function I want to declare a contract for

message_record_struct postSend(int destination, double* buf);

How do I declare a contract which allows assignment to the elements of send_count and send_queue?

I'm concerned the following approach only allows assignment to the element at the address of pointer to the array:

@ assigns send_count

And the following approach throws an error given the axiomatic theory { logic integer NP; } in an earlier portion of the code):

@ assigns *(send_count+(0..NP-1));
@ assigns \forall integer i; 0<=i<NP ==>                                                                                                                                                                
          *(send_count[i]+(0..NP-1));

$ frama-c -wp -wp-prover "why3ide" assign_example.c

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)

[kernel] Parsing assign_example.c (with preprocessing)

assign_example.c:62:[kernel] user error: syntax error (expression expected but predicate found) in annotation.

[kernel] user error: stopping on file "assign_example.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command.

[kernel] Frama-C aborted: invalid user input.
Solution

  • The syntax you are looking for is probably

    /*@ assigns *(send_count+(0..NP-1));
    assigns *(send_count[0..NP-1]+(0..NP-1));

    ACSL ranges [a..b] have been introduced to keep assigns clauses quantifiers-free, and should be used as much as possible.