[e-acsl:archi] add doc for Memory_observer

src/plugins/e-acsl/src/code_generator/memory_observer.ml

@@ -73,6 +73,6 @@ let delete_from_set ?before env kf vars =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/code_generator/memory_observer.mli

@@ -27,18 +27,23 @@ open Cil_types
 open Cil_datatype
 
 val store: ?before:stmt -> Env.t -> kernel_function -> varinfo list -> Env.t
+(** For each variable of the given list, if necessary according to the mmodel
+    analysis, add a call to [__e_acsl_store_block] in the given environment. *)
 
 val duplicate_store:
   ?before:stmt -> Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
+(** Same as [store], with a call to [__e_acsl_duplicate_store_block]. *)
 
 val delete_from_list:
   ?before:stmt -> Env.t -> kernel_function -> varinfo list -> Env.t
+(** Same as [store], with a call to [__e_acsl_delete_block]. *)
 
 val delete_from_set:
   ?before:stmt -> Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
+(** Same as [delete_from_list] with a set of variables instead of a list. *)
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)