diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml index a1b0106a43512a0cb8a4b521ae017c404d3fa455..f9cfa246d8a5669933d08bc833b43e20966e2abf 100644 --- a/src/kernel_services/ast_queries/logic_typing.ml +++ b/src/kernel_services/ast_queries/logic_typing.ml @@ -2312,6 +2312,10 @@ struct let check_lval_kind m t = let rec aux t = match t.term_node with | Tempty_set -> m.accept_empty + (* Be careful with const lval, cases are: + - *host* is variable -> the assigned *lval* must not be const + - host is memory access -> check if it is a const field access + *) | TLval (lhost,loff) -> (not (isLogicArrayType t.term_type) || m.accept_array) && (match lhost with @@ -2326,7 +2330,7 @@ struct model variables are not supported. *) | Some v -> (not v.vformal || m.accept_formal) && - (not (Cil.isConstType v.vtype) || m.accept_const) + (not (isConstType @@ logicCType t.term_type) || m.accept_const) end | TResult _ -> m.accept_models | _ -> true) && diff --git a/tests/spec/assigns_const.i b/tests/spec/assigns_const.i index 6aedfe366b91d48a081c137dd41a0ef09c3bb99b..b12e589cd954ce0aef0421fc5c9e0dea6ecf9215 100644 --- a/tests/spec/assigns_const.i +++ b/tests/spec/assigns_const.i @@ -29,3 +29,16 @@ void refuse_field_via_pointer(struct Y * ptr); //@ assigns *ptr ; void accept_const_via_pointer(int const * ptr); + +struct Z { + const int x; + int y; +}; + +static struct Z z; + +//@ assigns z.y; +void accept_partial_const_struct(void) +{ + z.y = 1; +} diff --git a/tests/spec/oracle/assigns_const.res.oracle b/tests/spec/oracle/assigns_const.res.oracle index 9279fd42e107faf983ef6d2e83d2b96081a57afd..3a2391c45fe329f7ca6a743d44a8f7b8254d0d34 100644 --- a/tests/spec/oracle/assigns_const.res.oracle +++ b/tests/spec/oracle/assigns_const.res.oracle @@ -16,6 +16,10 @@ struct X { struct Y { struct X a[10] ; }; +struct Z { + int const x ; + int y ; +}; int i; int const c; /*@ assigns i; */ @@ -26,4 +30,12 @@ struct Y y; /*@ assigns *ptr; */ void accept_const_via_pointer(int const *ptr); +static struct Z z; +/*@ assigns z.y; */ +void accept_partial_const_struct(void) +{ + z.y = 1; + return; +} +