diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml index 93889b764fe0adc88286eb2ee0cb9cc4757fe69f..22172b8226905770639e4a061c806538c283c7cd 100644 --- a/src/plugins/aorai/aorai_visitors.ml +++ b/src/plugins/aorai/aorai_visitors.ml @@ -41,14 +41,6 @@ let get_acceptance_pred () = | Bool3.False | Bool3.Undefined -> acc) Logic_const.pfalse st -let get_call_name exp = match exp.enode with - | Const(CStr(s)) -> s - | Lval(Var(vi),NoOffset) -> vi.vname - | _ -> - Aorai_option.not_yet_implemented - ~source:(fst exp.eloc) - "At this time, only explicit calls are allowed by the Aorai plugin." - (****************************************************************************) (* The instrumentation is done in two passes: diff --git a/src/plugins/aorai/path_analysis.ml b/src/plugins/aorai/path_analysis.ml index f1541639d21959fae9eb1b86545791f3f4882ac4..36c9ef735b4e94195ba1049f8a2785c69dc633b2 100644 --- a/src/plugins/aorai/path_analysis.ml +++ b/src/plugins/aorai/path_analysis.ml @@ -73,27 +73,6 @@ let dijkstra (adj: 'a -> ('a * int) list) (v1:'a) (v2:'a) = in loop (add (0,(v1,[])) (empty())) - - - -let existing_path (stl,_ as auto) stn1 stn2 = - let st1 = ref (List.hd stl) in - let st2 = ref (List.hd stl) in - List.iter - (fun st -> - if st.nums=stn1 then st1:=st; - if st.nums=stn2 then st2:=st; - ) - stl; - - try - let _ = dijkstra (voisins auto) !st1 !st2 in - true - with - | Not_found -> false -;; - - (** since Nitrogen-20111001 *) let get_transitions_of_state st (_,tr) = List.fold_left @@ -101,12 +80,6 @@ let get_transitions_of_state st (_,tr) = if tr.start.nums = st.nums then tr::acc else acc) [] tr -let get_transitions_to_state st (_,tr) = - List.fold_left - (fun acc tr -> - if tr.stop.nums = st.nums then tr::acc else acc) - [] tr - let get_edges st1 st2 (_,tr) = List.find_all (fun tr -> tr.start.nums = st1.nums && tr.stop.nums = st2.nums) @@ -131,16 +104,6 @@ let at_most_one_path (states,transitions as auto) st1 st2 = false with Not_found -> true -let test (stl,_ as auto) = - let st2 = List.hd stl in - let st1 = List.hd (List.tl stl) in - Aorai_option.feedback "test : Etats choisis (%d,%d)" st1.nums st2.nums; - let (res,_) = dijkstra (voisins auto) st1 st2 in - Aorai_option.feedback "Fini.@\n%a" - (Pretty_utils.pp_list ~pre:"@[[" ~sep:",@ " ~suf:"@]]" - (fun fmt st -> Format.fprintf fmt "%d" st.nums)) - res - (* Local Variables: compile-command: "make -C ../../.." diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml index d4db56dd55e79a133dad6f92106fab87ddff4f69..87b196e921f3af940d818b60c191f789d62e6e51 100644 --- a/src/plugins/aorai/utils_parser.ml +++ b/src/plugins/aorai/utils_parser.ml @@ -43,61 +43,3 @@ let newline lexbuf = let pos = lexbuf.lex_curr_p in lexbuf.lex_curr_p <- { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum } - -let rec get_last_field my_field my_offset = - match my_offset with - | Cil_types.NoOffset -> my_field - | Cil_types.Field(fieldinfo,the_offset) -> get_last_field fieldinfo the_offset - | _ -> Aorai_option.fatal "NOT YET IMPLEMENTED : struct with array access." - - -let rec add_offset father_offset new_offset = - match father_offset with - | Cil_types.NoOffset -> new_offset - | Cil_types.Field(_,the_offset) -> (Cil.addOffset father_offset (add_offset the_offset new_offset)) - | _ -> Aorai_option.fatal "NOT YET IMPLEMENTED : struct with array access." - - - -let rec get_field_info_from_name my_list name = - if(List.length my_list <> 0) then begin - let my_field = List.hd my_list in - if(my_field.Cil_types.fname = name) then my_field - else get_field_info_from_name (List.tl my_list) name - end - else Aorai_option.fatal "no field found with name :%s" name - - - -let get_new_offset my_host my_offset name= - match my_host with - | Cil_types.Var(var) -> - let var_info = var in - (* if my_offset is null no need to search the last field *) - (* else we need to have the last *) - - let my_comp = - if (my_offset = Cil_types.NoOffset) then - match var_info.Cil_types.vtype with - | Cil_types.TComp(mc,_,_) -> mc - | _ -> assert false - (*Cil_types.TComp(my_comp,_,_) = var_info.Cil_types.vtype in*) - - else begin - let get_field_from_offset my_offset = begin - match my_offset with - | Cil_types.Field(fieldinfo,_) -> fieldinfo - | _ -> Aorai_option.fatal "support only struct no array with struct" - end in - let field_info = get_field_from_offset my_offset in - let last_field_offset = get_last_field field_info my_offset in - (* last field in offset but not the field we want, for that we search in*) - let mc = last_field_offset.Cil_types.fcomp in - mc - end - in - let cfields = Option.value ~default:[] my_comp.Cil_types.cfields in - let field_info = get_field_info_from_name cfields name in - Cil_types.Field(field_info,Cil_types.NoOffset) - - | _ -> Aorai_option.fatal "NOT YET IMPLEMENTED : mem is not supported"