diff --git a/.Makefile.lint b/.Makefile.lint
index e9056d2e216fb962a7e5f928aa6c3cf864b4bb78..6feefd8e7db75131a329db0cf888e456e877942b 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -321,20 +321,3 @@ ML_LINT_KO+=src/plugins/value_types/precise_locs.ml
ML_LINT_KO+=src/plugins/value_types/value_types.ml
ML_LINT_KO+=src/plugins/value_types/value_types.mli
ML_LINT_KO+=src/plugins/value_types/widen_type.ml
-ML_LINT_KO+=src/plugins/variadic/classify.ml
-ML_LINT_KO+=src/plugins/variadic/environment.ml
-ML_LINT_KO+=src/plugins/variadic/extends.ml
-ML_LINT_KO+=src/plugins/variadic/extends.mli
-ML_LINT_KO+=src/plugins/variadic/format_parser.ml
-ML_LINT_KO+=src/plugins/variadic/format_parser.mli
-ML_LINT_KO+=src/plugins/variadic/format_pprint.ml
-ML_LINT_KO+=src/plugins/variadic/format_string.ml
-ML_LINT_KO+=src/plugins/variadic/format_typer.ml
-ML_LINT_KO+=src/plugins/variadic/format_typer.mli
-ML_LINT_KO+=src/plugins/variadic/format_types.mli
-ML_LINT_KO+=src/plugins/variadic/generic.ml
-ML_LINT_KO+=src/plugins/variadic/options.ml
-ML_LINT_KO+=src/plugins/variadic/standard.ml
-ML_LINT_KO+=src/plugins/variadic/translate.ml
-ML_LINT_KO+=src/plugins/variadic/va_build.ml
-ML_LINT_KO+=src/plugins/variadic/va_types.mli
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index a1d6848f595df84afff1eca16b6b568e44c521fd..3b7ec0011a82cccbe8d9d79a2839679608d3ef69 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1454,6 +1454,8 @@ src/plugins/variadic/generic.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/replacements.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/replacements.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/standard.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/translate.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/va_build.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index 2bd938cda21263d2a4fdb23d062c289fe65df8c9..1bf27b2b54704dd4d9dc598448a9440d7d0adc1b 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -49,38 +49,38 @@ let mk_aggregator env fun_name a_pos pname a_type =
match find_function env fun_name with
| None -> Misc
| Some vi ->
- try
- (* Get the list of arguments *)
- let params = Typ.params vi.vtype in
-
- (* Check that pos is a valid position in the list *)
- assert (a_pos >= 0);
- if a_pos >= List.length params then begin
- Self.warning ~current:true
- "The standard function %s should have at least %d parameters."
- fun_name
- (a_pos + 1);
- raise Exit
- end;
-
- (* Get the aggregate type of elements *)
- let _,ptyp,_ = List.nth params a_pos in
- let a_param = pname, match ptyp with
+ try
+ (* Get the list of arguments *)
+ let params = Typ.params vi.vtype in
+
+ (* Check that pos is a valid position in the list *)
+ assert (a_pos >= 0);
+ if a_pos >= List.length params then begin
+ Self.warning ~current:true
+ "The standard function %s should have at least %d parameters."
+ fun_name
+ (a_pos + 1);
+ raise Exit
+ end;
+
+ (* Get the aggregate type of elements *)
+ let _,ptyp,_ = List.nth params a_pos in
+ let a_param = pname, match ptyp with
| TArray (typ,_,_,_)
| TPtr (typ, _) -> typ
| _ ->
- Self.warning ~current:true
- "The parameter %d of standard function %s should be \
- of array type."
- (a_pos + 1)
- fun_name;
- raise Exit
- in
+ Self.warning ~current:true
+ "The parameter %d of standard function %s should be \
+ of array type."
+ (a_pos + 1)
+ fun_name;
+ raise Exit
+ in
- Aggregator {a_target = vi; a_pos; a_type; a_param}
+ Aggregator {a_target = vi; a_pos; a_type; a_param}
- (* In case of failure return Misc (apply generic translation) *)
- with Exit -> Misc
+ (* In case of failure return Misc (apply generic translation) *)
+ with Exit -> Misc
let mk_format_fun vi f_kind f_buffer ~format_pos =
let buffer_arguments = match f_buffer with
@@ -92,16 +92,16 @@ let mk_format_fun vi f_kind f_buffer ~format_pos =
let n_expected_args = (List.fold_left max (-1) expected_args) + 1
and n_actual_args = List.length (Typ.params vi.vtype) in
if n_actual_args < n_expected_args then
- begin
- Self.warning ~current:true
- "The standard function %s was expected to have at least %d fixed \
- parameters but only has %d.@ \
- No variadic translation will be performed."
- vi.vname
- n_expected_args
- n_actual_args;
- Misc
- end
+ begin
+ Self.warning ~current:true
+ "The standard function %s was expected to have at least %d fixed \
+ parameters but only has %d.@ \
+ No variadic translation will be performed."
+ vi.vname
+ n_expected_args
+ n_actual_args;
+ Misc
+ end
else
FormatFun { f_kind ; f_buffer ; f_format_pos = format_pos }
@@ -113,11 +113,11 @@ let mk_format_fun vi f_kind f_buffer ~format_pos =
let classify_std env vi = match vi.vname with
(* fcntl.h - Overloads of functions *)
| "fcntl" -> mk_overload env
- ["__va_fcntl_void" ; "__va_fcntl_int" ; "__va_fcntl_flock"]
+ ["__va_fcntl_void" ; "__va_fcntl_int" ; "__va_fcntl_flock"]
| "open" -> mk_overload env
- ["__va_open_void" ; "__va_open_mode_t"]
+ ["__va_open_void" ; "__va_open_mode_t"]
| "openat" -> mk_overload env
- ["__va_openat_void" ; "__va_openat_mode_t"]
+ ["__va_openat_void" ; "__va_openat_mode_t"]
(* unistd.h *)
| "execl" -> mk_aggregator env "execv" 1 "argv" EndedByNull
@@ -165,4 +165,3 @@ let classify env vi =
}
end else
None
-
diff --git a/src/plugins/variadic/environment.ml b/src/plugins/variadic/environment.ml
index 1165b7c21fb7f31bfb05e9bc11b0615636fc9272..c00e98d5d201115637138a8ac91a90392a780070 100644
--- a/src/plugins/variadic/environment.ml
+++ b/src/plugins/variadic/environment.ml
@@ -25,24 +25,24 @@ open Cil_types
module Table = Datatype.String.Hashtbl
type env =
-{
- globals: varinfo Table.t;
- functions: varinfo Table.t;
- typedefs: typeinfo Table.t;
- structs: compinfo Table.t;
- unions: compinfo Table.t;
- enums: enuminfo Table.t;
-}
+ {
+ globals: varinfo Table.t;
+ functions: varinfo Table.t;
+ typedefs: typeinfo Table.t;
+ structs: compinfo Table.t;
+ unions: compinfo Table.t;
+ enums: enuminfo Table.t;
+ }
let empty () : env =
-{
- globals = Table.create 17;
- functions = Table.create 17;
- typedefs = Table.create 17;
- structs = Table.create 17;
- unions = Table.create 17;
- enums = Table.create 17;
-}
+ {
+ globals = Table.create 17;
+ functions = Table.create 17;
+ typedefs = Table.create 17;
+ structs = Table.create 17;
+ unions = Table.create 17;
+ enums = Table.create 17;
+ }
let add_global (env : env) (vi : varinfo) : unit =
Table.add env.globals vi.vname vi
@@ -95,19 +95,19 @@ let from_file (file : file) : env =
let v = object inherit Cil.nopCilVisitor
method! vglob glob =
begin match glob with
- | GFunDecl(_,vi,_) | GFun ({svar = vi}, _) ->
- add_function env vi
- | GVarDecl (vi,_) | GVar (vi, _, _) ->
- add_global env vi
- | GType (typeinfo,_) ->
- add_typeinfo env typeinfo
- | GCompTag (compinfo,_) ->
- add_compinfo env compinfo
- | GEnumTag (enuminfo,_) ->
- add_enuminfo env enuminfo
- | _ -> ()
+ | GFunDecl(_,vi,_) | GFun ({svar = vi}, _) ->
+ add_function env vi
+ | GVarDecl (vi,_) | GVar (vi, _, _) ->
+ add_global env vi
+ | GType (typeinfo,_) ->
+ add_typeinfo env typeinfo
+ | GCompTag (compinfo,_) ->
+ add_compinfo env compinfo
+ | GEnumTag (enuminfo,_) ->
+ add_enuminfo env enuminfo
+ | _ -> ()
end;
- Cil.SkipChildren
+ Cil.SkipChildren
end in
Cil.visitCilFile v file;
env
diff --git a/src/plugins/variadic/extends.ml b/src/plugins/variadic/extends.ml
index 36dd5299909971e7e78d91cbadaa4172d8802014..679eb4a6c2e99eec57392e7be63a884a27b66472 100644
--- a/src/plugins/variadic/extends.ml
+++ b/src/plugins/variadic/extends.ml
@@ -70,13 +70,13 @@ module Cil = struct
let doublePtrType = ptrType doubleType
let signedIntegerTypes = [Cil.charType; shortType; Cil.intType;
- Cil.longType; longLongType]
+ Cil.longType; longLongType]
let unsignedIntegerTypes = [ucharType; ushortType; Cil.uintType;
- Cil.ulongType; Cil.ulongLongType]
+ Cil.ulongType; Cil.ulongLongType]
let signedIntegerPtrTypes = [Cil.charPtrType; shortPtrType; Cil.intPtrType;
- longPtrType; longlongPtrType]
+ longPtrType; longlongPtrType]
let unsignedIntegerPtrTypes = [ucharPtrType; ushortPtrType; Cil.uintPtrType;
- ulongPtrType; ulonglongPtrType]
+ ulongPtrType; ulonglongPtrType]
let signed_integers_ranking =
Extlib.mapi (fun i t -> (t, i)) signedIntegerTypes
@@ -95,13 +95,13 @@ module Cil = struct
let integer_ranking_comp t1 t2 =
let rt1, rt2 =
if is_signed_integer_type t1 && is_signed_integer_type t2 then
- List.assoc t1 signed_integers_ranking,
- List.assoc t2 signed_integers_ranking
+ List.assoc t1 signed_integers_ranking,
+ List.assoc t2 signed_integers_ranking
else if is_unsigned_integer_type t1 && is_unsigned_integer_type t2 then
- List.assoc t1 unsigned_integers_ranking,
- List.assoc t2 unsigned_integers_ranking
+ List.assoc t1 unsigned_integers_ranking,
+ List.assoc t2 unsigned_integers_ranking
else
- raise (Invalid_argument "rank_comp") in
+ raise (Invalid_argument "rank_comp") in
rt1 - rt2
let integer_promotion t1 t2 =
@@ -140,54 +140,54 @@ module List = struct
else a :: make (n - 1) a
let to_scalar = function
- | [a] -> a
- | _ -> failwith "to_scalar"
+ | [a] -> a
+ | _ -> failwith "to_scalar"
let of_opt = function
- | None -> []
- | Some x -> [x]
+ | None -> []
+ | Some x -> [x]
let to_opt = function
- | [] -> None
- | [a] -> Some a
- | _ -> failwith "to_opt"
+ | [] -> None
+ | [a] -> Some a
+ | _ -> failwith "to_opt"
let first = function
- | [] -> failwith "first"
- | a :: _ -> a
+ | [] -> failwith "first"
+ | a :: _ -> a
exception EmptyList
let rec last = function
- | [] -> raise EmptyList
- | [a] -> a
- | _ :: l -> last l
+ | [] -> raise EmptyList
+ | [a] -> a
+ | _ :: l -> last l
let rec take n l =
if n <= 0 then []
else match l with
- | [] -> []
- | a :: l -> a :: take (n - 1) l
+ | [] -> []
+ | a :: l -> a :: take (n - 1) l
let rec drop n l =
if n <= 0 then l
else match l with
- | [] -> []
- | _ :: l -> drop (n - 1) l
+ | [] -> []
+ | _ :: l -> drop (n - 1) l
let rec break n l =
if n <= 0 then ([], l)
else match l with
- | [] -> ([], [])
- | a :: l ->
+ | [] -> ([], [])
+ | a :: l ->
let l1, l2 = break (n - 1) l in
(a :: l1, l2)
let rec filter_map f = function
- | [] -> []
- | a :: l -> match f a with
- | Some r -> r :: filter_map f l
- | None -> filter_map f l
+ | [] -> []
+ | a :: l -> match f a with
+ | Some r -> r :: filter_map f l
+ | None -> filter_map f l
let iteri f l =
let i = ref 0 in
@@ -200,45 +200,45 @@ module List = struct
let rev_mapi f l =
let i = ref 0 in
let rec aux acc = function
- | [] -> acc
- | a :: l -> let a' = f !i a in incr i; aux (a' :: acc) l
+ | [] -> acc
+ | a :: l -> let a' = f !i a in incr i; aux (a' :: acc) l
in aux [] l
let iteri2 f l1 l2 =
let i = ref 0 in
let rec aux l1 l2 = match l1, l2 with
- | [], [] -> ()
- | a1 :: l1, a2 :: l2 -> f !i a1 a2; incr i; aux l1 l2
- | _, _ -> invalid_arg "List.iteri2"
+ | [], [] -> ()
+ | a1 :: l1, a2 :: l2 -> f !i a1 a2; incr i; aux l1 l2
+ | _, _ -> invalid_arg "List.iteri2"
in
aux l1 l2
let mapi2 f l1 l2 =
let i = ref 0 in
let rec aux l1 l2 = match l1, l2 with
- | [], [] -> []
- | a1 :: l1, a2 :: l2 -> let r = f !i a1 a2 in incr i; r :: aux l1 l2
- | _, _ -> invalid_arg "List.mapi2"
+ | [], [] -> []
+ | a1 :: l1, a2 :: l2 -> let r = f !i a1 a2 in incr i; r :: aux l1 l2
+ | _, _ -> invalid_arg "List.mapi2"
in
aux l1 l2
let reduce_left f l =
let rec aux acc = function
- | [] -> acc
- | a :: l -> aux (f acc a) l
+ | [] -> acc
+ | a :: l -> aux (f acc a) l
in match l with
| [] -> failwith "reduce"
| a :: l -> aux a l
let rec reduce_right f = function
- | [] -> failwith "reduce"
- | [a] -> a
- | a :: l -> f a (reduce_right f l)
+ | [] -> failwith "reduce"
+ | [a] -> a
+ | a :: l -> f a (reduce_right f l)
let map_fold_left f acc l =
let rec aux acc r = function
- | [] -> List.rev r, acc
- | a :: l ->
+ | [] -> List.rev r, acc
+ | a :: l ->
let a, acc = f acc a in
aux acc (a :: r) l
in
@@ -254,9 +254,9 @@ module List = struct
let rec unique_sorted cmp = function
- | a1 :: a2 :: l when cmp a1 a2 = 0 -> unique_sorted cmp (a2 :: l)
- | [] -> []
- | a :: l -> a :: unique_sorted cmp l
+ | a1 :: a2 :: l when cmp a1 a2 = 0 -> unique_sorted cmp (a2 :: l)
+ | [] -> []
+ | a :: l -> a :: unique_sorted cmp l
let sort_unique cmp l =
unique_sorted cmp (sort cmp l)
diff --git a/src/plugins/variadic/extends.mli b/src/plugins/variadic/extends.mli
index fc4af12f94877df709ff85ce10dc91ba6a4b6bfa..a3ce5afa58afd73c2eec46a017cf4ba907a27599 100644
--- a/src/plugins/variadic/extends.mli
+++ b/src/plugins/variadic/extends.mli
@@ -144,4 +144,3 @@ module List : sig
(** [replace i v l] returns a new list where [l.(i)] = [v] *)
val replace : int -> 'a -> 'a list -> 'a list
end
-
diff --git a/src/plugins/variadic/format_parser.ml b/src/plugins/variadic/format_parser.ml
index 3a31e59fe0b3c507c6b0c106ec05366089c89327..f656b33b44ee33065981770a28da211dd12e9d95 100644
--- a/src/plugins/variadic/format_parser.ml
+++ b/src/plugins/variadic/format_parser.ml
@@ -40,40 +40,40 @@ let check_flag spec flag =
match flag, cs with
| FSharp, #has_alternative_form -> true
| FZero, #integer_specifier when Extlib.has_some spec.f_precision ->
- warn "Flag 0 is ignored when a precision is specified"; false
+ warn "Flag 0 is ignored when a precision is specified"; false
| FZero, #numeric_specifier when List.mem FMinus spec.f_flags ->
- warn "Flag 0 is ignored when flag - is also specified."; false
+ warn "Flag 0 is ignored when flag - is also specified."; false
| FZero, #numeric_specifier -> true
| FMinus, cs when cs <> `n -> true
| FSpace, #signed_specifier when List.mem FPlus spec.f_flags ->
- warn "Flag ' ' is ignored when flag + is also specified."; false
+ warn "Flag ' ' is ignored when flag + is also specified."; false
| FSpace, #signed_specifier -> true
| FPlus, (#signed_specifier | #float_specifier) -> true
- | _ ->
- warn "Flag %a and conversion specififer %a are not compatibles."
- pp_flag flag
- pp_cs (spec.f_conversion_specifier,spec.f_capitalize);
- raise Invalid_format
+ | _ ->
+ warn "Flag %a and conversion specififer %a are not compatibles."
+ pp_flag flag
+ pp_cs (spec.f_conversion_specifier,spec.f_capitalize);
+ raise Invalid_format
let check_cs_compatibility cs capitalized has_field_width has_precision =
match cs with
| (`n | `c | `p) as cs when has_precision ->
- warn "Conversion specifier %a does not expect a precision."
- pp_cs (cs, capitalized) ;
- raise Invalid_format
+ warn "Conversion specifier %a does not expect a precision."
+ pp_cs (cs, capitalized) ;
+ raise Invalid_format
| `n when has_field_width ->
- warn "Conversion specifier n does not expect a field width.";
- raise Invalid_format
+ warn "Conversion specifier n does not expect a field width.";
+ raise Invalid_format
| _ -> ()
let rec make_flags_unique = function
| [] -> []
| f :: l ->
- if List.mem f l then (
- warn "Multiple usage of flag '%a'." pp_flag f;
- make_flags_unique l
- ) else
- f :: make_flags_unique l
+ if List.mem f l then (
+ warn "Multiple usage of flag '%a'." pp_flag f;
+ make_flags_unique l
+ ) else
+ f :: make_flags_unique l
(* When checking, we don't really care which type are returned but only if
it can be returned *)
@@ -147,27 +147,27 @@ struct
let get (s,i : t) : char =
try let c = Format_string.get_char s !i in incr i; c
with Format_string.OutOfBounds -> '\000'
- | Format_string.NotAscii _ -> '\026'
+ | Format_string.NotAscii _ -> '\026'
let last (s,i : t) : char =
try Format_string.get_char s (!i - 1)
with Format_string.OutOfBounds -> '\000'
- | Format_string.NotAscii _ -> '\026'
+ | Format_string.NotAscii _ -> '\026'
let peek (s,i : t) : char =
try Format_string.get_char s !i
with Format_string.OutOfBounds -> '\000'
- | Format_string.NotAscii _ -> '\026'
+ | Format_string.NotAscii _ -> '\026'
let getall (f : char -> bool) (s,i as b : t) : string =
let start = !i in
let len = ref 0 in
begin try
- while f (get b) do
- incr len;
- done;
- back b; (* last char has not been matched *)
- with _ -> ()
+ while f (get b) do
+ incr len;
+ done;
+ back b; (* last char has not been matched *)
+ with _ -> ()
end;
Format_string.sub_string s start !len
end
@@ -203,10 +203,10 @@ let parse_assignement_suppression b =
let rec parse_flags b =
match Buffer.get b with
| '-' -> FMinus :: parse_flags b
- | '+' -> FPlus :: parse_flags b
- | ' ' -> FSpace :: parse_flags b
- | '#' -> FSharp :: parse_flags b
- | '0' -> FZero :: parse_flags b
+ | '+' -> FPlus :: parse_flags b
+ | ' ' -> FSpace :: parse_flags b
+ | '#' -> FSharp :: parse_flags b
+ | '0' -> FZero :: parse_flags b
| _ -> Buffer.back b; []
let parse_f_fw b =
@@ -223,11 +223,11 @@ let parse_s_fw b =
let parse_precision b =
match Buffer.peek b with
| '.' -> Buffer.consume b; Some
- begin match Buffer.peek b with
- | '*' -> Buffer.consume b; PStar
- | '-' | '0'..'9'-> PInt (parse_int b)
- | _ -> PInt 0
- end
+ begin match Buffer.peek b with
+ | '*' -> Buffer.consume b; PStar
+ | '-' | '0'..'9'-> PInt (parse_int b)
+ | _ -> PInt 0
+ end
| _ -> None
let parse_lm b =
@@ -244,11 +244,11 @@ let parse_lm b =
let parse_brackets_interior b =
let first = ref true and circ = ref false in
- let matching = function
- | ']' when not !first -> false
- | '^' when !first && not !circ -> circ := true; true
- | '\000' -> warn "Unterminated brackets."; raise Invalid_format
- | _ -> first := false; true
+ let matching = function
+ | ']' when not !first -> false
+ | '^' when !first && not !circ -> circ := true; true
+ | '\000' -> warn "Unterminated brackets."; raise Invalid_format
+ | _ -> first := false; true
in
let s = Buffer.getall matching b in
Buffer.consume b;
@@ -270,14 +270,14 @@ let parse_f_cs b =
| 'g' | 'G' -> `g
| 'a' | 'A' -> `a
| '\000' ->
- warn "Missing conversion specifier at the end of format.";
- raise Invalid_format
+ warn "Missing conversion specifier at the end of format.";
+ raise Invalid_format
| '\026' ->
- warn "Conversion specifiers must be ascii characters.";
- raise Invalid_format
+ warn "Conversion specifiers must be ascii characters.";
+ raise Invalid_format
| c ->
- warn "Unknown conversion specifier %c." c;
- raise Invalid_format
+ warn "Unknown conversion specifier %c." c;
+ raise Invalid_format
let parse_s_cs b =
match Buffer.peek b with
@@ -320,4 +320,3 @@ let parse_s_format s = parse_aux parse_s_spec (Buffer.create s)
let parse_format typ s = match typ with
| PrintfLike -> FFormat (parse_f_format s)
| ScanfLike -> SFormat (parse_s_format s)
-
diff --git a/src/plugins/variadic/format_parser.mli b/src/plugins/variadic/format_parser.mli
index bf8937e1f7e4f1784c4cb1105c221c56c5f9b62f..10218a76d6b724d37131f218c33535f982f0cafc 100644
--- a/src/plugins/variadic/format_parser.mli
+++ b/src/plugins/variadic/format_parser.mli
@@ -33,4 +33,3 @@ val check_format : format -> format
val parse_f_format : Format_string.t -> f_format
val parse_s_format : Format_string.t -> s_format
val parse_format : format_kind -> Format_string.t -> format
-
diff --git a/src/plugins/variadic/format_pprint.ml b/src/plugins/variadic/format_pprint.ml
index 90d2d42f90fcd6bedec489c7f1614af951625b72..d1890a1d2ff4cbcab949d64989aff5fc0055cf30 100644
--- a/src/plugins/variadic/format_pprint.ml
+++ b/src/plugins/variadic/format_pprint.ml
@@ -120,12 +120,12 @@ let pp_s_specification ff (spec: s_conversion_specification) =
let pp_f_format ff fl =
let fl = Extends.List.filter_map
- (function | Specification s -> Some s | _ -> None) fl in
+ (function | Specification s -> Some s | _ -> None) fl in
Pretty_utils.pp_list ~sep:"@." (fun ff s -> pp_f_specification ff s) ff fl
let pp_s_format ff (fl: s_format) =
let fl = Extends.List.filter_map
- (function | Specification s -> Some s | _ -> None) fl in
+ (function | Specification s -> Some s | _ -> None) fl in
Pretty_utils.pp_list ~sep:"@." (fun ff s -> pp_s_specification ff s) ff fl
let pp_format ff = function
diff --git a/src/plugins/variadic/format_string.ml b/src/plugins/variadic/format_string.ml
index 6efa2326f69c8be67dc63949b08667bde229a421..f27b7431f4c47877fd5d507e623bd58776764d5c 100644
--- a/src/plugins/variadic/format_string.ml
+++ b/src/plugins/variadic/format_string.ml
@@ -21,8 +21,8 @@
(**************************************************************************)
type t =
-| String of string
-| WString of int64 list
+ | String of string
+ | WString of int64 list
exception OutOfBounds
exception NotAscii of int64
@@ -30,13 +30,13 @@ exception NotAscii of int64
let get_char (s : t) (i : int) : char =
match s with
| String s ->
- begin try
+ begin try
String.get s i
with
Invalid_argument _ -> raise OutOfBounds
- end
+ end
| WString s ->
- begin try
+ begin try
let c = List.nth s i in
if (c >= Int64.zero && c<= (Int64.of_int 255)) then
Char.chr (Int64.to_int c)
@@ -44,22 +44,22 @@ let get_char (s : t) (i : int) : char =
raise (NotAscii c)
with
Failure _ -> raise OutOfBounds
- end
+ end
let get_wchar (s : t) (i : int) : int64 =
match s with
| String s ->
- begin try
+ begin try
Int64.of_int (Char.code (String.get s i))
with
Invalid_argument _ -> raise OutOfBounds
- end
+ end
| WString s ->
- begin try
+ begin try
List.nth s i
with
Failure _ -> raise OutOfBounds
- end
+ end
let sub_string (s : t) (start : int) (len : int) : string =
let init_char i =
diff --git a/src/plugins/variadic/format_typer.ml b/src/plugins/variadic/format_typer.ml
index 318f48b1791d25adf40b3854e22cf54ba36c19a9..d37c1ef006064bd984d5507aaec36021433b6b31 100644
--- a/src/plugins/variadic/format_typer.ml
+++ b/src/plugins/variadic/format_typer.ml
@@ -35,7 +35,7 @@ type typdef_finder = Logic_typing.type_namespace -> string -> Cil_types.typ
let get_typedef ?(find_typedef = Globals.Types.find_type) s =
- try
+ try
find_typedef Logic_typing.Typedef s
with Not_found ->
raise (Type_not_found s)
@@ -119,17 +119,17 @@ let type_f_format ?find_typedef format =
let add_types spec =
match spec with
| Char _ -> ()
- | Specification s ->
- if s.f_field_width = Some `FWStar then
- r := (Cil.intType, `ArgIn) :: !r;
- if s.f_precision = Some PStar then
- r := (Cil.intType, `ArgIn) :: !r;
- let dir = match s.f_conversion_specifier with
- | `s -> `ArgInArray s.f_precision
- | `n -> `ArgOut
- | _ -> `ArgIn
- in
- r := (type_f_specifier ?find_typedef s, dir) :: !r;
+ | Specification s ->
+ if s.f_field_width = Some `FWStar then
+ r := (Cil.intType, `ArgIn) :: !r;
+ if s.f_precision = Some PStar then
+ r := (Cil.intType, `ArgIn) :: !r;
+ let dir = match s.f_conversion_specifier with
+ | `s -> `ArgInArray s.f_precision
+ | `n -> `ArgOut
+ | _ -> `ArgIn
+ in
+ r := (type_f_specifier ?find_typedef s, dir) :: !r;
in
List.iter add_types format;
List.rev !r
@@ -139,13 +139,13 @@ let type_s_format ?find_typedef format =
let add_types spec =
match spec with
| Char _ -> ()
- | Specification s ->
- let dir = match s.s_conversion_specifier with
- | `s -> `ArgOutArray
- | _ -> `ArgOut
- in
- if not s.s_assignment_suppression then
- r := (type_s_specifier ?find_typedef s, dir) :: !r;
+ | Specification s ->
+ let dir = match s.s_conversion_specifier with
+ | `s -> `ArgOutArray
+ | _ -> `ArgOut
+ in
+ if not s.s_assignment_suppression then
+ r := (type_s_specifier ?find_typedef s, dir) :: !r;
in
List.iter add_types format;
List.rev !r
@@ -154,4 +154,3 @@ let type_s_format ?find_typedef format =
let type_format ?find_typedef = function
| FFormat f -> type_f_format ?find_typedef f
| SFormat s -> type_s_format ?find_typedef s
-
diff --git a/src/plugins/variadic/format_typer.mli b/src/plugins/variadic/format_typer.mli
index bc78bb447eb3ec55920e126ebfa6991a418c8703..cb83a6fb9fbaf5c6bccbfb2325b294a588413385 100644
--- a/src/plugins/variadic/format_typer.mli
+++ b/src/plugins/variadic/format_typer.mli
@@ -38,4 +38,3 @@ val type_s_specifier : ?find_typedef : typdef_finder -> s_conversion_specificati
val type_f_format : ?find_typedef : typdef_finder -> f_format -> (typ * arg_dir) list
val type_s_format : ?find_typedef : typdef_finder -> s_format -> (typ * arg_dir) list
val type_format : ?find_typedef : typdef_finder -> format -> (typ * arg_dir) list
-
diff --git a/src/plugins/variadic/format_types.mli b/src/plugins/variadic/format_types.mli
index 5e8a6594abee98f0da36d823283a12ee08c29696..3bd4808e6122c543124a146408bcdb1974e45cf5 100644
--- a/src/plugins/variadic/format_types.mli
+++ b/src/plugins/variadic/format_types.mli
@@ -25,7 +25,7 @@
type flag = FMinus | FPlus | FSpace | FSharp | FZero
type flags = flag list
-type f_field_width = [ `FWStar | `FWInt of int (** positive integer *)]
+type f_field_width = [ `FWStar | `FWInt of int (** positive integer *)]
type s_field_width = [ `FWInt of int ]
type any_field_width = [ f_field_width | s_field_width ]
@@ -45,7 +45,7 @@ type f_conversion_specifier =
[ numeric_specifier | `c | `s | `p | `n ]
type s_conversion_specifier =
[ f_conversion_specifier | `Brackets of string ]
-type any_conversion_specifier =
+type any_conversion_specifier =
[ s_conversion_specifier | f_conversion_specifier ]
type f_conversion_specification = {
@@ -66,8 +66,8 @@ type s_conversion_specification = {
(** A format element is either a character or a conversion specification. *)
type 'spec token =
-| Char of char
-| Specification of 'spec
+ | Char of char
+ | Specification of 'spec
type f_format = f_conversion_specification token list
type s_format = s_conversion_specification token list
diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index edc982c19508e3a72dd06e123079fd218e7f62ea..d7298e5b82029e29df4500a8fe4aeba123e0cd67 100644
--- a/src/plugins/variadic/generic.ml
+++ b/src/plugins/variadic/generic.ml
@@ -39,7 +39,7 @@ let vpar =
(* Translation of variadic types (not deeply) *)
let translate_type = function
-| TFun (ret_typ, args, is_variadic, attributes) ->
+ | TFun (ret_typ, args, is_variadic, attributes) ->
let new_args =
if is_variadic
then
@@ -47,11 +47,11 @@ let translate_type = function
Some (ng_args @ [vpar] @ g_args)
else args
in
- TFun (ret_typ, new_args, false, attributes)
+ TFun (ret_typ, new_args, false, attributes)
-| TBuiltin_va_list attr -> vpar_typ attr
+ | TBuiltin_va_list attr -> vpar_typ attr
-| typ -> typ
+ | typ -> typ
(* Adding the vpar parameter to variadic functions *)
@@ -60,49 +60,49 @@ let add_vpar vi =
let formals = Cil.getFormalsDecl vi in
(* Add the vpar formal once *)
if not (List.exists (fun vi -> vi.vname = vpar_name) formals) then
- begin
- (* Register the new formal *)
- let new_formal = Cil.makeFormalsVarDecl vpar in
- let new_formals = formals @ [new_formal] in
- Cil.unsafeSetFormalsDecl vi new_formals
- end
+ begin
+ (* Register the new formal *)
+ let new_formal = Cil.makeFormalsVarDecl vpar in
+ let new_formals = formals @ [new_formal] in
+ Cil.unsafeSetFormalsDecl vi new_formals
+ end
(* Translation of va_* builtins *)
let translate_va_builtin caller inst =
let vi, args, loc = match inst with
- | Call(_, {enode = Lval(Var vi, _)}, args, loc) ->
+ | Call(_, {enode = Lval(Var vi, _)}, args, loc) ->
vi, args, loc
- | _ -> assert false
+ | _ -> assert false
in
let translate_va_start () =
let va_list = match args with
- | [{enode=Lval va_list}] -> va_list
- | _ -> Self.fatal "Unexpected arguments to va_start"
+ | [{enode=Lval va_list}] -> va_list
+ | _ -> Self.fatal "Unexpected arguments to va_start"
and varg =
try Extlib.last (Cil.getFormalsDecl caller.svar)
- with Invalid_argument _ -> Self.abort
- "Using va_start macro in a function which is not variadic."
+ with Invalid_argument _ ->
+ Self.abort "Using va_start macro in a function which is not variadic."
in
[ Set (va_list, Cil.evar ~loc varg, loc) ]
in
let translate_va_copy () =
let dest, src = match args with
- | [{enode=Lval dest}; src] -> dest, src
- | _ -> Self.fatal "Unexpected arguments to va_copy"
+ | [{enode=Lval dest}; src] -> dest, src
+ | _ -> Self.fatal "Unexpected arguments to va_copy"
in
[ Set (dest, src, loc) ]
in
let translate_va_arg () =
let va_list, typ, lval = match args with
- | [{enode=Lval va_list};
- {enode=SizeOf typ};
- {enode=CastE(_, {enode=AddrOf lval})}] -> va_list, typ, lval
- | _ -> Self.fatal "Unexpected arguments to va_arg"
+ | [{enode=Lval va_list};
+ {enode=SizeOf typ};
+ {enode=CastE(_, {enode=AddrOf lval})}] -> va_list, typ, lval
+ | _ -> Self.fatal "Unexpected arguments to va_arg"
in
(* Check validity of type *)
if Cil.isIntegralType typ then begin
@@ -119,7 +119,7 @@ let translate_va_builtin caller inst =
(* Build the replacing instruction *)
let mk_lval_exp lval = Cil.new_exp ~loc (Lval lval) in
let mk_mem exp = mk_lval_exp (Cil.mkMem ~addr:exp ~off:NoOffset) in
- let mk_cast exp typ = Cil.mkCast ~force:false ~e:exp ~newt:typ in
+ let mk_cast exp typ = Cil.mkCast ~force:false ~e:exp ~newt:typ in
let src = mk_mem (mk_cast (mk_mem (mk_lval_exp va_list)) (TPtr (typ,[])))
in
[ Set (lval, src, loc);
@@ -127,11 +127,11 @@ let translate_va_builtin caller inst =
in
begin match vi.vname with
- | "__builtin_va_start" -> translate_va_start ()
- | "__builtin_va_copy" -> translate_va_copy ()
- | "__builtin_va_arg" -> translate_va_arg ()
- | "__builtin_va_end" -> [] (* No need to do anything for va_end *)
- | _ -> assert false
+ | "__builtin_va_start" -> translate_va_start ()
+ | "__builtin_va_copy" -> translate_va_copy ()
+ | "__builtin_va_arg" -> translate_va_arg ()
+ | "__builtin_va_end" -> [] (* No need to do anything for va_end *)
+ | _ -> assert false
end
@@ -166,7 +166,7 @@ let translate_call ~fundec ~ghost block loc mk_call callee pars =
(* Build an array to store addresses *)
let addrs = List.map Cil.mkAddrOfVi vis in
let vargs, assigns = Build.array_init ~loc fundec ~ghost block
- "__va_args" Cil.voidPtrType addrs
+ "__va_args" Cil.voidPtrType addrs
in
let instrs = instrs @ [assigns] in
diff --git a/src/plugins/variadic/options.ml b/src/plugins/variadic/options.ml
index 3558df1885504ed9bbfda4bb10677f9e9df04042..352a1faf08f2cb92b8667558b43e1e39593ecf64 100644
--- a/src/plugins/variadic/options.ml
+++ b/src/plugins/variadic/options.ml
@@ -21,24 +21,24 @@
(**************************************************************************)
module Self = Plugin.Register
- (struct
- let name = "Variadic"
- let shortname = "variadic"
- let help = "Variadic functions translation"
- end)
+ (struct
+ let name = "Variadic"
+ let shortname = "variadic"
+ let help = "Variadic functions translation"
+ end)
module Enabled = Self.True
- (struct
- let option_name = "-variadic-translation"
- let help = "translate variadic functions and calls to semantic \
- equivalents with only a fixed list of formal parameters"
- end)
+ (struct
+ let option_name = "-variadic-translation"
+ let help = "translate variadic functions and calls to semantic \
+ equivalents with only a fixed list of formal parameters"
+ end)
module Strict = Self.True
- (struct
- let option_name = "-variadic-strict"
- let help = "display warnings about non-portable implicit casts in the \
- calls of standard variadic functions, i.e. casts between \
- distinct integral types which have the same size and \
- signedness"
- end)
+ (struct
+ let option_name = "-variadic-strict"
+ let help = "display warnings about non-portable implicit casts in the \
+ calls of standard variadic functions, i.e. casts between \
+ distinct integral types which have the same size and \
+ signedness"
+ end)
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 996987ac14da81f0a71d19ec1a639ed3f03237f5..27ed9f5e4baa3bd328d8961603b00d5cc1fa9d40 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -134,7 +134,7 @@ let cast_arg i paramtyp exp =
The argument will be cast from %a to %a."
(i + 1)
pretty_typ argtyp pretty_typ paramtyp
- end;
+ end;
Cil.mkCast ~force:false ~e:exp ~newt:paramtyp
@@ -181,12 +181,12 @@ let find_null exp_list =
let aggregator_call
~fundec ~ghost {a_target; a_pos; a_type; a_param} scope loc mk_call vf args =
let name = vf.vf_decl.vorig_name
- and tparams = Typ.params_types a_target.vtype
+ and tparams = Typ.params_types a_target.vtype
and pname, ptyp = a_param in
(* Check argument count *)
let argcount = List.length args
- and paramcount = List.length tparams in
+ and paramcount = List.length tparams in
if argcount < paramcount then begin
Self.warning ~current:true
"Not enough arguments: expected %d, given %d."
@@ -195,14 +195,14 @@ let aggregator_call
end;
(* Compute the size of the aggregation *)
- let size = match a_type with
- | EndedByNull ->
+ let size = match a_type with
+ | EndedByNull ->
begin try
- find_null (List.drop a_pos args) + 1
- with Not_found ->
- Self.warning ~current:true
- "Failed to find a sentinel (NULL pointer) in the argument list.";
- raise Translate_call_exn;
+ find_null (List.drop a_pos args) + 1
+ with Not_found ->
+ Self.warning ~current:true
+ "Failed to find a sentinel (NULL pointer) in the argument list.";
+ raise Translate_call_exn;
end
in
@@ -272,24 +272,24 @@ let overloaded_call ~fundec overload block loc mk_call vf args =
let tparams, new_callee =
match filter_matching_prototypes overload args with
| [] -> (* No matching prototype *)
- Self.warning ~current:true
- "@[No matching prototype found for this call to %s.@.\
- Expected candidates:@.\
- @[<v> %a@]@.\
- Given arguments:@.\
- @[<v> %a@]"
- name (pp_overload name) overload
- (pp_prototype name) (List.map Cil.typeOf args);
- raise Translate_call_exn;
+ Self.warning ~current:true
+ "@[No matching prototype found for this call to %s.@.\
+ Expected candidates:@.\
+ @[<v> %a@]@.\
+ Given arguments:@.\
+ @[<v> %a@]"
+ name (pp_overload name) overload
+ (pp_prototype name) (List.map Cil.typeOf args);
+ raise Translate_call_exn;
| [(tparams,vi)] -> (* Exactly one matching prototype *)
- tparams, vi
+ tparams, vi
| l -> (* Several matching prototypes *)
- Self.warning ~current:true
- "Ambiguous call to %s. Matching candidates are: \
- %a"
- name
- (pp_overload name) l;
- raise Translate_call_exn;
+ Self.warning ~current:true
+ "Ambiguous call to %s. Matching candidates are: \
+ %a"
+ name
+ (pp_overload name) l;
+ raise Translate_call_exn;
in
(* Store the translation *)
@@ -331,7 +331,7 @@ let find_predicate name =
| [] ->
Self.warning ~once:true
"Unable to locate ACSL predicate %s which should be in the Frama-C LibC. \
- Correct specifications can't be generated."
+ Correct specifications can't be generated."
name;
None
@@ -396,17 +396,17 @@ let build_fun_spec env loc vf format_fun tvparams formals =
let add_lval ~indirect (lval,dir) =
(* Add the lval to the list of sources/dests *)
begin match dir with
- | (`ArgIn | `ArgInArray _) -> insert_source ~indirect lval
- | (`ArgOut | `ArgOutArray) -> insert_dest lval
- | `ArgInOut -> insert_source ~indirect lval; insert_dest lval
+ | (`ArgIn | `ArgInArray _) -> insert_source ~indirect lval
+ | (`ArgOut | `ArgOutArray) -> insert_dest lval
+ | `ArgInOut -> insert_source ~indirect lval; insert_dest lval
end
in
let add_var ?pos (vi,dir) =
(* Use the appropriate logical lval *)
let lval = match dir with
- | `ArgIn -> Build.lvar vi
- | (`ArgInArray _ | `ArgOutArray) -> Build.trange_from_vi ~loc vi
- | (`ArgOut | `ArgInOut) -> Build.tvarmem ~loc vi
+ | `ArgIn -> Build.lvar vi
+ | (`ArgInArray _ | `ArgOutArray) -> Build.trange_from_vi ~loc vi
+ | (`ArgOut | `ArgInOut) -> Build.tvarmem ~loc vi
in
(* Build requires/ensures *)
let term = Build.tvar ~loc vi in
@@ -477,17 +477,17 @@ let build_fun_spec env loc vf format_fun tvparams formals =
(* assigns stream->__fc_FILE_data
\from stream->__fc_FILE_data, __fc_FILE_id *)
begin match find_field env "__fc_FILE" "__fc_FILE_data" with
- | Some fieldinfo ->
+ | Some fieldinfo ->
let varfield = Build.tvarfield ~loc vi fieldinfo in
add_lval ~indirect:false (varfield, `ArgInOut)
- | None ->
+ | None ->
add_var ~indirect:false (vi, `ArgInOut)
end;
begin match find_field env "__fc_FILE" "__fc_FILE_id" with
- | Some fieldinfo ->
+ | Some fieldinfo ->
let varfield = Build.tvarfield ~loc vi fieldinfo in
add_lval ~indirect:true (varfield, `ArgIn)
- | None -> ()
+ | None -> ()
end
in
@@ -527,31 +527,31 @@ let build_fun_spec env loc vf format_fun tvparams formals =
in
begin match format_fun.f_buffer, format_fun.f_kind with
- | StdIO, ScanfLike ->
+ | StdIO, ScanfLike ->
begin match find_global env "__fc_stdin" with
- | Some vi -> add_stream vi
- | None -> ()
+ | Some vi -> add_stream vi
+ | None -> ()
end
- | StdIO, PrintfLike ->
+ | StdIO, PrintfLike ->
begin match find_global env "__fc_stdout" with
- | Some vi -> add_stream vi
- | None -> ()
+ | Some vi -> add_stream vi
+ | None -> ()
end
- | Arg (i, _), ScanfLike ->
+ | Arg (i, _), ScanfLike ->
add_var ~indirect:true (List.nth sformals i, `ArgInArray None)
- | Arg (i, size_pos), PrintfLike ->
+ | Arg (i, size_pos), PrintfLike ->
add_var ~indirect:true (List.nth sformals i, `ArgOutArray);
begin match size_pos with
- | Some n ->
- add_buffer (List.nth sformals i) (List.nth sformals n)
- | None -> ()
+ | Some n ->
+ add_buffer (List.nth sformals i) (List.nth sformals n)
+ | None -> ()
end
- | Stream i, _ ->
+ | Stream i, _ ->
add_stream (List.nth sformals i)
- | File i, _ ->
+ | File i, _ ->
let file = List.nth sformals i in
add_var ~indirect:true (file, `ArgIn);
- | Syslog, _ -> ()
+ | Syslog, _ -> ()
end;
(* Build the assigns clause (without \result, for now; it will be added
@@ -571,7 +571,7 @@ let build_fun_spec env loc vf format_fun tvparams formals =
(* Build the default behaviour *)
let bhv = Cil.mk_behavior ~assigns
- ~requires:!requires ~post_cond:!ensures () in
+ ~requires:!requires ~post_cond:!ensures () in
{ (Cil.empty_funspec ()) with spec_behavior = [bhv] }
@@ -582,7 +582,7 @@ let format_fun_call ~fundec env format_fun scope loc mk_call vf args =
and params = Typ.params vf.vf_decl.vtype in
(* Remove the va_param parameter added during the declaration visit *)
let fixed_params_count = Typ.params_count vf.vf_original_type in
- let sparams = List.take fixed_params_count params in
+ let sparams = List.take fixed_params_count params in
(* Extract the format if possible *)
let format =
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 2f09a846eb26e980ea7ccc4cde8337829e466308..627221bc47962ca15d63ee417388d4a05826f8ee 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -45,7 +45,7 @@ let translate_variadics (file : file) =
(* Environment filled with global symbols. *)
let env = Environment.from_file file in
- (* Table associating varinfo of variadic functions to a variadic_function
+ (* Table associating varinfo of variadic functions to a variadic_function
description *)
let module Table = Cil_datatype.Varinfo.Hashtbl in
let classification : variadic_function Table.t = Table.create 17 in
@@ -54,14 +54,14 @@ let translate_variadics (file : file) =
method! vglob glob =
begin match glob with
- | GFunDecl(_, vi, _) | GFun ({svar = vi}, _)
- when not (is_framac_builtin vi) ->
+ | GFunDecl(_, vi, _) | GFun ({svar = vi}, _)
+ when not (is_framac_builtin vi) ->
if not (Table.mem classification vi) then begin
let vf = Classify.classify env vi in
may (Table.add classification vi) vf
end;
Cil.SkipChildren
- | _ ->
+ | _ ->
Cil.SkipChildren
end
end
@@ -88,26 +88,26 @@ let translate_variadics (file : file) =
(* Translate types and signatures *)
method! vglob glob =
begin match glob with
- | GFunDecl(_, vi, _) when is_framac_builtin vi ->
+ | GFunDecl(_, vi, _) when is_framac_builtin vi ->
Self.result ~level:2 ~current:true
"Variadic builtin %s left untransformed." vi.vname;
Cil.SkipChildren
- | GFunDecl(_, vi, _) ->
+ | GFunDecl(_, vi, _) ->
if Table.mem classification vi then
Generic.add_vpar vi;
Cil.DoChildren
- | GFun ({svar = vi} as fundec, _) ->
+ | GFun ({svar = vi} as fundec, _) ->
if Table.mem classification vi then begin
Generic.add_vpar vi;
fundec.sformals <- Cil.getFormalsDecl vi;
end;
Standard.new_globals := [];
Cil.DoChildrenPost (fun globs ->
- List.rev (globs @ !Standard.new_globals))
+ List.rev (globs @ !Standard.new_globals))
- | _ ->
+ | _ ->
Cil.DoChildren
end
@@ -156,83 +156,90 @@ let translate_variadics (file : file) =
~fundec ~ghost block loc mk_call (Cil.evar ~loc f) args
in
begin match i with
- | Call(_, {enode = Lval(Var vi, _)}, _, _)
- when List.mem vi.vname va_builtins ->
+ | Call(_, {enode = Lval(Var vi, _)}, _, _)
+ when List.mem vi.vname va_builtins ->
File.must_recompute_cfg fundec;
Cil.ChangeTo (Generic.translate_va_builtin fundec i)
- | Call(lv, {enode = Lval(Var vi, NoOffset)}, args, loc) ->
- begin
- try
+ | Call(lv, {enode = Lval(Var vi, NoOffset)}, args, loc) ->
+ begin
+ try
+ let mk_call f args = Call (lv, f, args, loc) in
+ let res = make_new_args mk_call vi args in
+ File.must_recompute_cfg fundec;
+ Cil.ChangeTo res
+ with Not_found ->
+ Cil.DoChildren
+ end
+
+ | Call(lv, callee, args, loc) ->
+ let is_variadic =
+ try
+ let args, _ = Typ.ghost_partitioned_params (Cil.typeOf callee) in
+ let last = Extends.List.last args in
+ last = Generic.vpar
+ with Extends.List.EmptyList -> false
+ in
+ if is_variadic then begin
let mk_call f args = Call (lv, f, args, loc) in
- let res = make_new_args mk_call vi args in
+ let res =
+ Generic.translate_call
+ ~fundec
+ ~ghost
+ block
+ loc
+ mk_call
+ callee
+ args
+ in
File.must_recompute_cfg fundec;
Cil.ChangeTo res
- with Not_found ->
+ end else
Cil.DoChildren
- end
-
- | Call(lv, callee, args, loc) ->
- let is_variadic =
- try
- let args, _ = Typ.ghost_partitioned_params (Cil.typeOf callee) in
- let last = Extends.List.last args in
- last = Generic.vpar
- with Extends.List.EmptyList -> false
- in
- if is_variadic then begin
- let mk_call f args = Call (lv, f, args, loc) in
- let res =
- Generic.translate_call ~fundec ~ghost block loc mk_call callee args
- in
- File.must_recompute_cfg fundec;
- Cil.ChangeTo res
- end else
- Cil.DoChildren
- | Local_init(v, ConsInit(c, args, kind), loc) ->
- begin
- try
- let mk_call f args =
- let args =
- match kind, args with
- | Constructor, [] ->
- Options.Self.fatal
- "Constructor %a is expected to have at least one argument"
- Cil_printer.pp_varinfo c
- | Constructor, _::tl -> tl
- | Plain_func, args -> args
- in
- let f =
- match f.enode with
- | Lval (Var f, NoOffset) -> f
- | _ ->
- Options.Self.fatal
- "Constructor cannot be translated as indirect call"
+ | Local_init(v, ConsInit(c, args, kind), loc) ->
+ begin
+ try
+ let mk_call f args =
+ let args =
+ match kind, args with
+ | Constructor, [] ->
+ Options.Self.fatal
+ "Constructor %a is expected to have at least one argument"
+ Cil_printer.pp_varinfo c
+ | Constructor, _::tl -> tl
+ | Plain_func, args -> args
+ in
+ let f =
+ match f.enode with
+ | Lval (Var f, NoOffset) -> f
+ | _ ->
+ Options.Self.fatal
+ "Constructor cannot be translated as indirect call"
+ in
+ Local_init(v,ConsInit(f,args,kind),loc)
in
- Local_init(v,ConsInit(f,args,kind),loc)
- in
- let args =
- match kind with
+ let args =
+ match kind with
| Plain_func -> args
| Constructor -> Cil.mkAddrOfVi v :: args
- in
- let res = make_new_args mk_call c args in
- File.must_recompute_cfg fundec;
- Cil.ChangeTo res
- with Not_found ->
- Cil.DoChildren
- end
- | _-> Cil.DoChildren
+ in
+ let res = make_new_args mk_call c args in
+ File.must_recompute_cfg fundec;
+ Cil.ChangeTo res
+ with Not_found ->
+ Cil.DoChildren
+ end
+ | _-> Cil.DoChildren
end
method! vexpr exp =
begin match exp.enode with
- | AddrOf (Var vi, NoOffset)
- when Extends.Cil.is_variadic_function vi && is_framac_builtin vi ->
+ | AddrOf (Var vi, NoOffset)
+ when Extends.Cil.is_variadic_function vi && is_framac_builtin vi ->
Self.not_yet_implemented
"The variadic plugin doesn't handle calls to a pointer to the \
variadic builtin %s."
vi.vname
- | _ -> Cil.DoChildren
+ | _ -> Cil.DoChildren
end
end
in
diff --git a/src/plugins/variadic/va_build.ml b/src/plugins/variadic/va_build.ml
index 101a8fa5c99bd8c414b12be2ad8bd8ac47429adb..c33f058e41b3a9287ab02d9f03728b33c46a8bc3 100644
--- a/src/plugins/variadic/va_build.ml
+++ b/src/plugins/variadic/va_build.ml
@@ -48,11 +48,11 @@ let array_init ~loc fundec ~ghost scope name elem_typ values =
let vi = Cil.makeLocalVar fundec ~ghost ~scope name typ in
let initl =
match values with
- | [] -> [ Index (Cil.zero ~loc, NoOffset), Cil.makeZeroInit ~loc elem_typ]
- | _ ->
- List.mapi
- (fun i exp -> Index (Cil.integer ~loc i, NoOffset), SingleInit exp)
- values
+ | [] -> [ Index (Cil.zero ~loc, NoOffset), Cil.makeZeroInit ~loc elem_typ]
+ | _ ->
+ List.mapi
+ (fun i exp -> Index (Cil.integer ~loc i, NoOffset), SingleInit exp)
+ values
in
vi.vdefined <- true;
vi, Local_init(vi, AssignInit(CompoundInit(typ,initl)), loc)
@@ -106,7 +106,7 @@ exception NotAFunction
let tapp ~loc logic_info labels args =
let ltyp = match logic_info.l_type with
- | None -> raise NotAFunction
- | Some ltyp -> ltyp
+ | None -> raise NotAFunction
+ | Some ltyp -> ltyp
in
Logic_const.term ~loc (Tapp (logic_info, labels, args)) ltyp
diff --git a/src/plugins/variadic/va_types.mli b/src/plugins/variadic/va_types.mli
index 74aa2086327cc463e7a5a84dc456bb3b81e4a8d8..70063338550ae6ea4ca452d6c679b1c8649128ae 100644
--- a/src/plugins/variadic/va_types.mli
+++ b/src/plugins/variadic/va_types.mli
@@ -24,28 +24,28 @@ open Cil_types
type variadic_class =
-| Unknown
-(** Function declared and not known by Frama-C *)
-| Defined
-(** Function for which we have the definition in the project *)
-| Misc
-(** Function from the Frama-C lib *)
-| Overload of overload
-(** Function from the Frama-C lib which declines into a finite number of
- possible prototypes whose names are given in the list *)
-| Aggregator of aggregator
-(** Function from the Frama-C lib which has a not-variadic equivalent with
- the variadic part replaced by an array. (The array is the aggregation of
- the arguments from the variadic part. *)
-| FormatFun of format_fun
-(** Function from the Frama-C lib for which the argument count and type is
- fixed by a format argument. *)
+ | Unknown
+ (** Function declared and not known by Frama-C *)
+ | Defined
+ (** Function for which we have the definition in the project *)
+ | Misc
+ (** Function from the Frama-C lib *)
+ | Overload of overload
+ (** Function from the Frama-C lib which declines into a finite number of
+ possible prototypes whose names are given in the list *)
+ | Aggregator of aggregator
+ (** Function from the Frama-C lib which has a not-variadic equivalent with
+ the variadic part replaced by an array. (The array is the aggregation of
+ the arguments from the variadic part. *)
+ | FormatFun of format_fun
+ (** Function from the Frama-C lib for which the argument count and type is
+ fixed by a format argument. *)
and overload = (typ list * varinfo) list
and aggregator = {
- a_target: varinfo;
- a_pos: int;
+ a_target: varinfo;
+ a_pos: int;
a_type: aggregator_type;
a_param: string * typ;
}
@@ -59,11 +59,11 @@ and format_fun = {
}
and buffer =
-| StdIO (** Standard input/output (stdin/stdout/stderr) *)
-| Arg of int * int option (* Position of the buffer and size arguments *)
-| Stream of int (* Position of the stream argument *)
-| File of int (* Position of the file argument *)
-| Syslog (* Output to some system log *)
+ | StdIO (** Standard input/output (stdin/stdout/stderr) *)
+ | Arg of int * int option (* Position of the buffer and size arguments *)
+ | Stream of int (* Position of the stream argument *)
+ | File of int (* Position of the file argument *)
+ | Syslog (* Output to some system log *)
type variadic_function = {
@@ -73,4 +73,3 @@ type variadic_function = {
mutable vf_specialization_count: int; (* The number of specializations of
this function built yet *)
}
-