[E-ACSL] new option -e-acsl-full-mmodel to monitor all pointers

src/plugins/e-acsl/TODO

@@ -21,6 +21,7 @@
 # KNOWN BUGS #
 ##############
 
+- see BTS
 - comparaisons qui aboutissent à du C incorrect
   ==> comparaison de chaînes litérales
    (voir tests other_constants.i et comparison.i)

src/plugins/e-acsl/options.ml

@@ -76,6 +76,13 @@ module Gmp_only =
       let help = ""
      end)
 
+module Full_mmodel =
+  False
+    (struct
+      let option_name = "-e-acsl-full-mmodel"
+      let help = ""
+     end)
+
 let () = Plugin.set_group help
 module Version =
   False

src/plugins/e-acsl/options.mli

@@ -29,6 +29,7 @@ module Run: Bool
 module Valid: Bool
 module Prepare: Bool
 module Gmp_only: Bool
+module Full_mmodel: Bool
 module Project_name: String
 
 val must_visit: unit -> bool

src/plugins/e-acsl/pre_analysis.ml

@@ -532,14 +532,17 @@ and must_model_exp ?kf ?stmt e = match e.enode with
   | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ 
   | AlignOfE _ -> assert false
 
-let must_model_vi ?kf ?stmt vi = 
-  Error.generic_handle (must_model_vi ?kf ?stmt) false vi
+let must_model_vi ?kf ?stmt vi =
+  Options.Full_mmodel.get ()
+  || Error.generic_handle (must_model_vi ?kf ?stmt) false vi
 
 let must_model_lval ?kf ?stmt lv = 
-  Error.generic_handle (must_model_lval ?kf ?stmt) false lv
+  Options.Full_mmodel.get ()
+  || Error.generic_handle (must_model_lval ?kf ?stmt) false lv
 
 let old_must_model_vi bhv ?kf ?stmt vi =
-  must_model_vi ?kf ?stmt (Cil.get_original_varinfo bhv vi)
+  Options.Full_mmodel.get ()
+  || must_model_vi ?kf ?stmt (Cil.get_original_varinfo bhv vi)
 
 (*
 Local Variables:

src/plugins/e-acsl/visit.ml

@@ -127,7 +127,7 @@ class e_acsl_visitor prj generate = object (self)
     let cur = Project.current () in
     let selection = 
       State_selection.of_list 
-	[ Options.Gmp_only.self; Options.Check.self;
+	[ Options.Gmp_only.self; Options.Check.self; Options.Full_mmodel.self;
 	  Kernel.SignedOverflow.self; Kernel.UnsignedOverflow.self;
 	  Kernel.SignedDowncast.self; Kernel.UnsignedDowncast.self;
 	  Kernel.Machdep.self ] 
@@ -135,9 +135,6 @@ class e_acsl_visitor prj generate = object (self)
     if generate then Project.copy ~selection ~src:cur prj;
     Cil.DoChildrenPost
       (fun f ->
-	(* reset them at the end to be observationally equivalent to a standard
-	   visitor. *)
-	if generate then Project.clear ~selection ~project:prj ();
 	(* extend the main with forward initialization and put it at end *)
 	if not (Options.Check.get ()) then begin
 	  let must_init =
@@ -243,6 +240,9 @@ you must call function `%s' by yourself"
 	    in
 	    Project.on prj build_initializer ()
 	end;
+	(* reset copied states at the end to be observationally equivalent to a
+	   standard visitor. *)
+	if generate then Project.clear ~selection ~project:prj ();
 	f)
 
   method vglob_aux = function