Merge remote-tracking branch 'origin/master' into feature/bobot/jbuilder

meta_annotate.ml

@@ -125,7 +125,7 @@ class context_visitor flags all_mp table = object(self)
       let pred = ump.ump_property kf ~stmt assoc_list in
       (* Apply potential post transformation *)
       let post_pred = match post with
-        | None -> pred 
+        | None -> pred
         | Some f -> f pred
       in
       (* Simplify *)
@@ -231,15 +231,10 @@ class weak_inv_visitor flags full_table table (pre, post) = object (self)
     Cil.SkipChildren
 end
 
-let ctype_of_tlval tlval =
-  let ltype = Cil.typeOfTermLval tlval in
-  Logic_utils.logicCType ltype
-
 (* Given a tlval, return the term taking its address *)
 let addr_of_tlval tlval =
-  let typ = ctype_of_tlval tlval in
-  let ntype = Logic_utils.coerce_type (TPtr (typ, [])) in
-  Logic_const.taddrof tlval ntype
+  let typ = Cil.typeOfTermLval tlval in
+  Logic_utils.mk_logic_AddrOf tlval typ
 
 (* Instantiate properties at any call site, replacing \called by
  * the called function. *)
@@ -270,7 +265,7 @@ class calling_visitor flags all_mp table = object (self)
     List.iter (self # instantiate stmt assoc_list) mp_todo
 
   method! vinst = function
-    | Call (_, fexpr, args, _) -> 
+    | Call (_, fexpr, args, _) ->
       let lv = match fexpr.enode with Lval lv -> lv | _ -> assert false in
       let stmt = Option.get self # current_stmt in
       let called_kf = Kernel_function.get_called fexpr in
@@ -290,7 +285,7 @@ let inspect_contract process stmt ckf args =
   let vis = object (_)
     inherit Visitor.frama_c_inplace
 
-    val fargs = 
+    val fargs =
       let h = Hashtbl.create (List.length args) in
       let _, oargs, _, _ = Cil.splitFunctionType
           (Kernel_function.get_type ckf) in
@@ -299,7 +294,7 @@ let inspect_contract process stmt ckf args =
           (Option.get oargs) args ;
       h
 
-    method! vterm _ = 
+    method! vterm _ =
       Cil.DoChildrenPost (fun term -> match term.term_node with
           | TLval (host, _) | TAddrOf (host, _) | TStartOf (host, _) ->
             begin match host with
@@ -328,7 +323,7 @@ let inspect_contract process stmt ckf args =
           clause. Assuming meta-properties with reading/writing contexts are \
           valid in this function." Kernel_function.pretty ckf
         | Writes l -> process ckf stmt vis l ass
-    ) ckf 
+    ) ckf
 
 (* Instantiate properties at any point where a modification can happen, that is:
  * - common assignments (including the result of a function)
@@ -353,7 +348,7 @@ class writing_visitor flags all_mp table = object(self)
         let propag = Visitor.visitFramacTerm vis term in
         if not @@ Logic_utils.contains_result propag then
           match propag.term_node with
-            | TLval t -> 
+            | TLval t ->
               let post prop =
                 List.fold_left (fun prop prec ->
                     Logic_const.pimplies (prec, prop)
@@ -365,7 +360,7 @@ class writing_visitor flags all_mp table = object(self)
 
   (* Instantiate an annotation for each affectation (potentially resulting
    * from a call) and each call to an undefined function *)
-  method! vstmt_aux stmt = 
+  method! vstmt_aux stmt =
     if not stmt.ghost then (
       match stmt.skind with
         | Instr Set (lval, _, _) ->
@@ -381,7 +376,7 @@ class writing_visitor flags all_mp table = object(self)
             self#writing_instance stmt tl
           ) ;
           (match Kernel_function.get_called fexp with
-            | Some ckf -> 
+            | Some ckf ->
               begin try
                 (* Function is implemented, do nothing *)
                 ignore (Kernel_function.get_definition ckf)
@@ -500,11 +495,11 @@ class reading_visitor flags all_mp table = object (self)
             | Some ckf -> self#passthrough_process stmt ckf args
             | None -> Self.warning
                         "%a The called function is not determined \
-                         but it could read from variables" Printer.pp_location loc 
+                         but it could read from variables" Printer.pp_location loc
           end
         | _ -> ()
       end ;
-      let after s = 
+      let after s =
         let set = StmtHashtbl.find_opt lvals_by_stmt s in
         if Option.is_some set then
           TLvalSet.iter (self#reading_instance s) @@ Option.get set
@@ -530,9 +525,9 @@ let lvals_of_predicate pred =
           | LBnone -> ()
           | LBinductive _
           | LBreads _ -> s := None
-          | LBpred p -> ignore (Visitor.visitFramacPredicate 
+          | LBpred p -> ignore (Visitor.visitFramacPredicate
                                   (self :> Visitor.frama_c_visitor) p)
-          | LBterm t -> ignore (Visitor.visitFramacTerm 
+          | LBterm t -> ignore (Visitor.visitFramacTerm
                                   (self :> Visitor.frama_c_visitor) t)
         end ; Cil.DoChildren
       | _ -> Cil.DoChildren
@@ -591,7 +586,7 @@ class strong_inv_visitor flags all_mp table = object (self)
           | None -> false
           | Some m -> self # possible_interference m ump
       in
-      if lenient || can_interfere then 
+      if lenient || can_interfere then
         self#instantiate ~force_after:true stmt [] ump
     in
     begin match stmt.skind with

tests/wp-cache/cache/0c8fb0f06d61ec099aac05ae2c74b694.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0035,
+  "steps": 22 }

tests/wp-cache/cache/36c2f07e1e21777d95ff0514a7e57e49.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "timeout", "time": 1. }

tests/wp-cache/cache/74897fcc7f8dbaa13236da778a144d6f.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.007,
+  "steps": 22 }

tests/wp-cache/cache/a752daddc9413c6ff7a6c283d3141694.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0053,
+  "steps": 22 }