do not monitor variables with incomplete types (fix bts #2406)

src/plugins/e-acsl/doc/Changelog

@@ -19,6 +19,8 @@
 #   configure	configure
 ###############################################################################
 
+-* E-ACSL       [2018/10/23] Fix bug #2406 about monitoring of variables
+	        with incomplete types.
 -* E-ACSL       [2018/10/04] Fix bug #2386 about incorrect typing when
                 performing pointer subtraction.
 -* E-ACSL       [2018/10/04] Support for \at on purely logic variables.

src/plugins/e-acsl/doc/userman/changes.tex

@@ -6,13 +6,15 @@ release. First we list changes of the last release.
 \section*{E-ACSL \eacslversion}
 
 \begin{itemize}
-\item \textbf{Introduction}: Improve a bit and reference related papers.
+\item \textbf{Introduction}: Improve a bit and reference new related papers.
 \item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
   not yet robust.
 \item \textbf{What the Plug-in Provides}: Highlight the importance of
   \textbf{-e-acsl-prepare}.
 \item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
   Monitoring Libraries'' by the new section ``Supported Systems''.
+\item \textbf{Known Limitations}: Add limitation about monitoring of variables 
+  with incomplete types.
 \end{itemize}
 
 \section*{E-ACSL Chlorine-20180501}

src/plugins/e-acsl/doc/userman/limitations.tex

@@ -143,8 +143,8 @@ instrumented code (linked against this main) could print some warnings from the
 \label{sec:limits:no-code}
 \index{Function!Undefined}
 
-The instrumentation in the generated program is partial for a program $p$ if and
-only if $p$ contains a memory-related annotation $a$ and an undefined function
+The instrumentation in the generated program is partial for a program $p$ if $p$
+contains a memory-related annotation $a$ and an undefined function 
 $f$ such that:
 \begin{itemize}
 \item either $f$ has an (even indirect) effect on a left-value occurring in $a$;
@@ -155,6 +155,15 @@ A violation of such an annotation $a$ is undetected. There is no workaround yet.
 Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
 undefined functions. There is also no workaround yet.
 
+\subsection{Incomplete Types}
+\index{Type!Incomplete}
+
+The instrumentation in the generated program is partial for a program $p$ if $p$
+contains a memory-related annotation $a$ and a variable $v$ with an incomplete
+type definition such that $a$ depends on $v$ (even indirectly).
+
+A violation of such an annotation $a$ is undetected. There is no workaround yet.
+
 \section{Recursive Functions}
 \index{Function!Recursive}
 

src/plugins/e-acsl/mmodel_analysis.ml

@@ -25,6 +25,15 @@ open Cil_datatype
 
 module Dataflow = Dataflow2
 
+let must_never_monitor vi =
+  (* extern ghost variables are usually used (by the Frama-C libc) to
+     represent some internal invisible states in ACSL specifications. They do
+     not correspond to something concrete *)
+  (vi.vghost && vi.vstorage = Extern)
+  ||
+    (* incomplete types cannot be properly monitored. See BTS #2406. *)
+    not (Cil.isCompleteType vi.vtype)
+
 (* ********************************************************************** *)
 (* Backward dataflow analysis to compute a sound over-approximation of what
    left-values must be tracked by the memory model library *)
@@ -225,16 +234,20 @@ module rec Transfer
 
   let extend_to_expr always state lhost e =
     let add_vi state vi =
-      if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state) then
+      if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state)
+      then begin
         match base_addr e with
         | None -> state
         | Some vi_e ->
-          Options.feedback ~level:4 ~dkey
-            "monitoring %a from %a."
-            Printer.pp_varinfo vi_e
-            Printer.pp_lval (lhost, NoOffset);
-          Varinfo.Hptset.add vi_e state
-      else
+          if must_never_monitor vi then state
+          else begin
+            Options.feedback ~level:4 ~dkey
+              "monitoring %a from %a."
+              Printer.pp_varinfo vi_e
+              Printer.pp_lval (lhost, NoOffset);
+            Varinfo.Hptset.add vi_e state
+          end
+      end else
         state
     in
     match lhost with
@@ -721,44 +734,70 @@ consolidated_must_model_vi vi
       false
  *)
 
-let rec must_model_lval bhv ?kf ?stmt = function
-  | Var vi, _ -> must_model_vi bhv ?kf ?stmt vi
-  | Mem e, _ -> must_model_exp bhv ?kf ?stmt e
+let rec apply_on_vi_base_from_lval f bhv ?kf ?stmt = function
+  | Var vi, _ -> f bhv ?kf ?stmt vi
+  | Mem e, _ -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
 
-and must_model_exp bhv ?kf ?stmt e = match e.enode with
+and apply_on_vi_base_from_exp f bhv ?kf ?stmt e = match e.enode with
   | Lval lv | AddrOf lv | StartOf lv ->
-    must_model_lval bhv ?kf ?stmt lv
+    apply_on_vi_base_from_lval f bhv ?kf ?stmt lv
   | BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) ->
-    must_model_exp bhv ?kf ?stmt e1
+    apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
   | BinOp(MinusPP, e1, e2, _) ->
-    must_model_exp bhv ?kf ?stmt e1 || must_model_exp bhv ?kf ?stmt e2
-  | Info(e, _) | CastE(_, e) -> must_model_exp bhv ?kf ?stmt e
+    apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
+    || apply_on_vi_base_from_exp f bhv ?kf ?stmt e2
+  | Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
   | BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt | Lt | Gt | Le
             | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
   | Const _ -> (* possible in case of static address *) false
   | UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
     Options.fatal "[pre_analysis] unexpected expression %a" Exp.pretty e
 
+let must_model_lval = apply_on_vi_base_from_lval must_model_vi
+let must_model_exp = apply_on_vi_base_from_exp must_model_vi
+
+let must_never_monitor_lval bhv ?kf ?stmt lv =
+  apply_on_vi_base_from_lval
+    (fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
+    bhv
+    ?kf
+    ?stmt
+    lv
+
+let must_never_monitor_exp bhv ?kf ?stmt lv  =
+  apply_on_vi_base_from_exp
+    (fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
+    bhv
+    ?kf
+    ?stmt
+    lv
+
 (* ************************************************************************** *)
 (** {1 Public API} *)
 (* ************************************************************************** *)
 
 let must_model_vi ?bhv ?kf ?stmt vi =
-  not (vi.vghost && vi.vstorage = Extern)
+  not (must_never_monitor vi)
   &&
     (Options.Full_mmodel.get ()
      || Error.generic_handle (must_model_vi bhv ?kf ?stmt) false vi)
 
 let must_model_lval ?bhv ?kf ?stmt lv =
-  Options.Full_mmodel.get ()
-  || Error.generic_handle (must_model_lval bhv ?kf ?stmt) false lv
+  not (must_never_monitor_lval bhv ?kf ?stmt lv)
+  &&
+    (Options.Full_mmodel.get ()
+     || Error.generic_handle (must_model_lval bhv ?kf ?stmt) false lv)
 
 let must_model_exp ?bhv ?kf ?stmt exp =
-  Options.Full_mmodel.get ()
-  || Error.generic_handle (must_model_exp bhv ?kf ?stmt) false exp
+  not (must_never_monitor_exp bhv ?kf ?stmt exp)
+  &&
+    (Options.Full_mmodel.get ()
+     || Error.generic_handle (must_model_exp bhv ?kf ?stmt) false exp)
 
-let use_model () = not (Env.is_empty ()) || Options.Full_mmodel.get () ||
-  Env.has_heap_allocations ()
+let use_model () =
+  not (Env.is_empty ())
+  || Options.Full_mmodel.get ()
+  || Env.has_heap_allocations ()
 
 (*
 Local Variables:

src/plugins/e-acsl/tests/bts/bts2406.c

+/* run.config
+   COMMENT: bts #2306, do not monitor incomplete types
+*/
+
+const char tab[]; /* not monitored */
+char t[10]; /* monitored */
+
+int main(void) {
+  char *p = tab; /* monitored */
+  /*@ assert !\valid(p+(0..9)); */
+  /*@ assert \valid(t+(0..9)); */
+  return 0;
+}

src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva] tests/bts/bts2406.c:5: Warning: 
+  during initialization of variable 'tab', size of type 'char const []'
+  cannot be computed (Size of array without number of elements.)

src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+char const tab[];
+char t[10];
+void __e_acsl_globals_init(void)
+{
+  __e_acsl_store_block((void *)(t),(size_t)10);
+  __e_acsl_full_init((void *)(& t));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_globals_init();
+  char *p = (char *)(tab);
+  __e_acsl_store_block((void *)(& p),(size_t)8);
+  __e_acsl_full_init((void *)(& p));
+  /*@ assert ¬\valid(p + (0 .. 9)); */
+  {
+    int __gen_e_acsl_valid;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(p + 1 * 0),(size_t)9,
+                                        (void *)p,(void *)(& p));
+    __e_acsl_assert(! __gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+                    (char *)"!\\valid(p + (0 .. 9))",10);
+  }
+  /*@ assert \valid(&t[0 .. 9]); */
+  {
+    int __gen_e_acsl_valid_2;
+    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& t + 1 * 0),(size_t)9,
+                                          (void *)(& t),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
+                    (char *)"\\valid(&t[0 .. 9])",11);
+  }
+  __retres = 0;
+  __e_acsl_delete_block((void *)(t));
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+