--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is it possible to use tsets returned by logic functions in assigns?



Hi

I am attempting to verify some code I am maintaining in FFmpeg. Section
"2.8.1 Finite sets" in the ACSL manual claims tsets can be used in
assigns clauses. But when I try to do so (via a logic function) I get
the following error:

  not an assignable left value: avio_assigns{Old}(s). Ignoring
specification of function avio_r8

My ACSL is as follows:

  /*@ predicate avio_valid(struct AVIOContext *s) = \valid(s);
      predicate avio_valid_read(AVIOContext *s) = \valid_read(s);
      logic set<char*> avio_assigns(AVIOContext *s) = {
        &s->buffer_size,
        s->buffer
      };
   */
  /*@ requires avio_valid(s);
      assigns avio_assigns(s);
      ensures 0 <= \result <= 255;
   */
  int          avio_r8  (AVIOContext *s);

The point of declaring avio_assigns() is of course to be able to reuse
and \union these tsets as one builds larger and larger call graphs.

What am I missing?

/Tomas