Update for Scandium

query.mli

@@ -20,7 +20,7 @@
 (**************************************************************************)
 
 val prepare: Project.t -> unit
-val add_sload: Cil.visitor_behavior -> Project.t -> unit
+val add_sload: Visitor_behavior.t -> Project.t -> unit
 val add_simulation: Project.t -> unit
 
 val original  : ('a -> 'b) -> 'a -> 'b

single_load.ml

@@ -44,7 +44,7 @@ class visitor bhv_ref prj = object(me)
   method private pr_vlval lv = Visitor.visitFramacLval (me :> copy) lv
   method private pr_voff  o  = Visitor.visitFramacOffset (me :> copy) o
 
-  method private pr_nvi vi = Cil.memo_varinfo me#behavior vi
+  method private pr_nvi vi = Visitor_behavior.Memo.varinfo me#behavior vi
 
   val mutable insert_ph = false
 
@@ -118,7 +118,7 @@ class visitor bhv_ref prj = object(me)
   method! vlval _ =
     let loc = Cil.CurrentLoc.get() in
     let nf = match me#current_func with
-      | Some(f) -> Cil.memo_fundec me#behavior f
+      | Some(f) -> Visitor_behavior.Memo.fundec me#behavior f
       | None -> assert false
     in
 

single_load.mli

@@ -19,4 +19,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val make : string -> (Project.t * Cil.visitor_behavior)
+val make : string -> (Project.t * Visitor_behavior.t)

specified_atomic.ml

@@ -40,8 +40,8 @@ let atomic_typer ~typing_context ~loc ps =
 (* Definition of atomic extension for ACSL *)
 (* check if the given behavior bhv contains "atomic" mention *)
 let is_atomic_behavior bhv =
-  let atomic b = match b with
-    | (_, "atomic", _, _, Ext_preds _) -> true
+  let atomic b = match b.ext_name, b.ext_kind with
+    | "atomic", Ext_preds _ -> true
     | _ -> false
   in
   List.exists atomic bhv.b_extended

statements.ml

@@ -410,15 +410,15 @@ let process_call_sites make_visitor =
 let process_ret_site make_visitor id site =
   let fid, res, stmt = match site with
     | LoadRet(i,r,s) ->
-      let r = Logic_utils.lval_to_term_lval ~cast:true r in
+      let r = Logic_utils.lval_to_term_lval r in
       i, (Some r), s
     | Ret(i, rvalue, s) ->
       if rvalue then
         let r = match (Functions.get_return_expression_of i).enode with
           | Lval(lv) -> lv
           | _ -> assert false
         in
-        let r = Logic_utils.lval_to_term_lval ~cast:true r in
+        let r = Logic_utils.lval_to_term_lval r in
         i, (Some r), s
       else
         i, None, s