diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index fcf4ab3aed662c046f0a69f2489eeb554f5ce7a3..6fe35aa0bbd78d55b382d51a67017a89b7cb0694 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2316,17 +2316,21 @@ struct
       accept_models: bool;
       accept_func_ptr: bool;
       accept_addrs: bool;
+      accept_const: bool;
     }
 
   let lval_addressable_mode =
     { accept_empty = false; accept_formal = true; accept_array = true;
-      accept_models = false; accept_func_ptr = true; accept_addrs = false;}
+      accept_models = false; accept_func_ptr = true; accept_addrs = false;
+      accept_const = true; }
   let lval_assignable_mode =
     { accept_empty = true; accept_formal = true; accept_array = false;
-      accept_models = true; accept_func_ptr = false; accept_addrs = false;}
+      accept_models = true; accept_func_ptr = false; accept_addrs = false;
+      accept_const = false; }
   let lval_assigns_dependency_mode =
     { accept_empty = true; accept_formal = true; accept_array = false;
-      accept_models = true; accept_func_ptr = false; accept_addrs = true;}
+      accept_models = true; accept_func_ptr = false; accept_addrs = true;
+      accept_const = true; }
 
   let is_fct_ptr lv = Cil.isLogicFunctionType (Cil.typeOfTermLval lv)
 
@@ -2345,12 +2349,15 @@ struct
                else
                  false (* pure logic variable, at least as long as
                           model variables are not supported. *)
-             | Some v -> not v.vformal || m.accept_formal
+             | Some v ->
+               (not v.vformal || m.accept_formal) &&
+               (not (Cil.isConstType v.vtype) || m.accept_const)
            end
          | TResult _ -> m.accept_models
          | _ -> true) &&
         (match snd (Logic_utils.remove_term_offset loff) with
          | TModel _ -> m.accept_models
+         | TField(f, _) -> not (Cil.isConstType f.ftype) || m.accept_const
          | _ -> true)
       | TAddrOf lv when is_fct_ptr lv -> m.accept_func_ptr
       | TAddrOf lv | TStartOf lv ->
@@ -3289,10 +3296,11 @@ struct
       (other_prms @ prms), p
     | _ -> [], ctxt.type_predicate ctxt env p0
 
-  let term_lval_assignable ctxt ~accept_formal env t =
+  let term_lval_assignable ctxt ~accept_formal ~accept_const env t =
     let module [@warning "-60"] C = struct end in
     let t = ctxt.type_term ctxt env t in
-    if not (check_lval_kind { lval_assignable_mode with accept_formal } t) then
+    let mode = { lval_assignable_mode with accept_formal ; accept_const } in
+    if not (check_lval_kind mode t) then
       ctxt.error t.term_loc "not an assignable left value: %a"
         Cil_printer.pp_term t;
     lift_set (term_lval (fun _ t -> t)) t
@@ -3500,7 +3508,7 @@ struct
     let module [@warning "-60"] C = struct end in
     (* Yannick: [assigns *\at(\result,Post)] should be allowed *)
     let tl =
-      term_lval_assignable ctxt ~accept_formal env l
+      term_lval_assignable ctxt ~accept_formal ~accept_const:false env l
     in
     let tl = Logic_const.new_identified_term tl in
     match d with
@@ -4210,8 +4218,10 @@ struct
       let env = Lenv.empty () in
       let ctxt = base_ctxt env in
       let tsets =
+        let accept_formal = false in
+        let accept_const  = true in
         List.map
-          (term_lval_assignable ctxt ~accept_formal:false env) tsets
+          (term_lval_assignable ctxt ~accept_formal ~accept_const env) tsets
       in
       let checks_tsets_type fct ctyp =
         List.iter
diff --git a/tests/spec/assigns_const.i b/tests/spec/assigns_const.i
new file mode 100644
index 0000000000000000000000000000000000000000..6aedfe366b91d48a081c137dd41a0ef09c3bb99b
--- /dev/null
+++ b/tests/spec/assigns_const.i
@@ -0,0 +1,31 @@
+int i ;
+int const c ;
+
+//@ assigns i ;
+void accept_non_const(void);
+
+//@ assigns c ;
+void refuse_const(void);
+
+const int a[2];
+
+//@ assigns a[0] ;
+void refuse_const_array(void);
+
+//@ assigns { i, c };
+void refuse_const_in_set(void);
+
+struct X { int const f; };
+struct Y { struct X a[10] ; };
+struct Y y ;
+
+//@ assigns y.a[4].f ;
+void refuse_const_field(void);
+
+//@ assigns (*ptr).a[4].f ;
+void refuse_field_via_pointer(struct Y * ptr);
+
+// Acceptable const assigns:
+
+//@ assigns *ptr ;
+void accept_const_via_pointer(int const * ptr);
diff --git a/tests/spec/oracle/assigns_const.res.oracle b/tests/spec/oracle/assigns_const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9279fd42e107faf983ef6d2e83d2b96081a57afd
--- /dev/null
+++ b/tests/spec/oracle/assigns_const.res.oracle
@@ -0,0 +1,29 @@
+[kernel] Parsing tests/spec/assigns_const.i (no preprocessing)
+[kernel:annot-error] tests/spec/assigns_const.i:7: Warning: 
+  not an assignable left value: c. Ignoring specification of function refuse_const
+[kernel:annot-error] tests/spec/assigns_const.i:12: Warning: 
+  not an assignable left value: a[0]. Ignoring specification of function refuse_const_array
+[kernel:annot-error] tests/spec/assigns_const.i:15: Warning: 
+  not an assignable left value: {i, c}. Ignoring specification of function refuse_const_in_set
+[kernel:annot-error] tests/spec/assigns_const.i:22: Warning: 
+  not an assignable left value: y.a[4].f. Ignoring specification of function refuse_const_field
+[kernel:annot-error] tests/spec/assigns_const.i:25: Warning: 
+  not an assignable left value: ptr->a[4].f. Ignoring specification of function refuse_field_via_pointer
+/* Generated by Frama-C */
+struct X {
+   int const f ;
+};
+struct Y {
+   struct X a[10] ;
+};
+int i;
+int const c;
+/*@ assigns i; */
+void accept_non_const(void);
+
+int const a[2];
+struct Y y;
+/*@ assigns *ptr; */
+void accept_const_via_pointer(int const *ptr);
+
+