--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2020 ---
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