[wp] Introduce a notion of coloring predicate

src/plugins/wp/Lang.ml

@@ -430,6 +430,7 @@ and model = {
   m_result : sort ;
   m_typeof : tau option list -> tau ;
   m_source : source ;
+  m_coloring : bool ;
 }
 
 and source =
@@ -448,6 +449,10 @@ let tau_of_lfun phi ts =
     | Sbool -> Bool
     | _ -> m.m_typeof ts
 
+let is_coloring_lfun = function
+  | ACSL _ | CTOR _ -> false
+  | Model { m_coloring } -> m_coloring
+
 type balance = Nary | Left | Right
 
 let not_found _ = raise Not_found
@@ -467,6 +472,7 @@ let symbolf
     ?(params=[])
     ?(sort=Logic.Sdata)
     ?(result:tau option)
+    ?(coloring=false)
     ?(typecheck:(tau option list -> tau) option)
     name =
   let buffer = Buffer.create 80 in
@@ -500,20 +506,21 @@ let symbolf
          m_result = result ;
          m_typeof = typeof ;
          m_source = source ;
+         m_coloring = coloring ;
        }
     ) (Format.formatter_of_buffer buffer) name
 
 let extern_s
-    ~library ?link ?category ?params ?sort ?result ?typecheck name =
+    ~library ?link ?category ?params ?sort ?result ?coloring ?typecheck name =
   symbolf
-    ~library ?category ?params ?sort ?result ?typecheck ?link "%s" name
+    ~library ?category ?params ?sort ?result ?coloring ?typecheck ?link "%s" name
 
 let extern_f
-    ~library ?link ?balance ?category ?params ?sort ?result ?typecheck name =
+    ~library ?link ?balance ?category ?params ?sort ?result ?coloring ?typecheck name =
   symbolf
-    ~library ?category ?params ?link ?balance ?sort ?result ?typecheck name
+    ~library ?category ?params ?link ?balance ?sort ?result ?coloring ?typecheck name
 
-let extern_p ~library ?bool ?prop ?link ?(params=[]) () =
+let extern_p ~library ?bool ?prop ?link ?(params=[]) ?(coloring=false) () =
   let link =
     match bool,prop,link with
     | Some b , Some p , None -> infoprover (Engine.F_bool_prop(b,p))
@@ -526,10 +533,11 @@ let extern_p ~library ?bool ?prop ?link ?(params=[]) () =
     m_params = params ;
     m_result = Logic.Sprop;
     m_typeof = not_found;
-    m_source = Extern (new_extern ~library ~link ~debug)
+    m_source = Extern (new_extern ~library ~link ~debug) ;
+    m_coloring = coloring ;
   }
 
-let extern_fp ~library ?(params=[]) ?link phi =
+let extern_fp ~library ?(params=[]) ?link ?(coloring=false) phi =
   let link = match link with
     | None -> infoprover (Engine.F_call phi)
     | Some link -> map_infoprover (fun phi -> Engine.F_call(phi)) link in
@@ -541,19 +549,21 @@ let extern_fp ~library ?(params=[]) ?link phi =
     m_source = Extern (new_extern
                          ~library
                          ~link
-                         ~debug:phi)
+                         ~debug:phi) ;
+    m_coloring = coloring ;
   }
 
-let generated_f ?context ?category ?params ?sort ?result name =
-  symbolf ?context ?category ?params ?sort ?result name
+let generated_f ?context ?category ?params ?sort ?result ?coloring name =
+  symbolf ?context ?category ?params ?sort ?result ?coloring name
 
-let generated_p ?context name =
+let generated_p ?context ?(coloring=false) name =
   Model {
     m_category = Logic.Function ;
     m_params = [] ;
     m_result = Logic.Sprop;
     m_typeof = not_found;
-    m_source = generated ?context name
+    m_source = generated ?context name ;
+    m_coloring = coloring ;
   }
 
 let extern_t name ~link ~library =

src/plugins/wp/Lang.mli

@@ -92,6 +92,7 @@ and model = {
   m_result : sort ;
   m_typeof : tau option list -> tau ;
   m_source : source ;
+  m_coloring : bool ;
 }
 
 and source =
@@ -123,6 +124,7 @@ val extern_s :
   ?params:sort list ->
   ?sort:sort ->
   ?result:tau ->
+  ?coloring:bool ->
   ?typecheck:(tau option list -> tau) ->
   string -> lfun
 
@@ -134,6 +136,7 @@ val extern_f :
   ?params:sort list ->
   ?sort:sort ->
   ?result:tau ->
+  ?coloring:bool ->
   ?typecheck:(tau option list -> tau) ->
   ('a,Format.formatter,unit,lfun) format4 -> 'a
 (** balance just give a default when link is not specified *)
@@ -144,16 +147,17 @@ val extern_p :
   ?prop:string ->
   ?link:Engine.link infoprover ->
   ?params:sort list ->
+  ?coloring:bool ->
   unit -> lfun
 
 val extern_fp : library:library -> ?params:sort list ->
-  ?link:string infoprover -> string -> lfun
+  ?link:string infoprover -> ?coloring:bool -> string -> lfun
 
 val generated_f : ?context:bool -> ?category:lfun category ->
-  ?params:sort list -> ?sort:sort -> ?result:tau ->
+  ?params:sort list -> ?sort:sort -> ?result:tau -> ?coloring:bool ->
   ('a,Format.formatter,unit,lfun) format4 -> 'a
 
-val generated_p : ?context:bool -> string -> lfun
+val generated_p : ?context:bool -> ?coloring:bool -> string -> lfun
 
 val extern_t:
   string -> link:string infoprover -> library:library -> mdt
@@ -193,6 +197,8 @@ val parameters : (lfun -> sort list) -> unit (** definitions *)
 val name_of_lfun : lfun -> string
 val name_of_field : field -> string
 
+val is_coloring_lfun : lfun -> bool
+
 (** {2 Logic Formulae} *)
 
 module ADT : Logic.Data with type t = adt