diff --git a/.Makefile.lint b/.Makefile.lint
index f213229e55714480b8766486a7538600f510672a..da13c5b801adb0d708f45d53ccdbb29c84280886 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -366,11 +366,6 @@ ML_LINT_KO+=src/plugins/postdominators/compute.ml
ML_LINT_KO+=src/plugins/postdominators/postdominators_parameters.ml
ML_LINT_KO+=src/plugins/postdominators/print.ml
ML_LINT_KO+=src/plugins/print_api/print_interface.ml
-ML_LINT_KO+=src/plugins/rte/generator.ml
-ML_LINT_KO+=src/plugins/rte/options.ml
-ML_LINT_KO+=src/plugins/rte/register.ml
-ML_LINT_KO+=src/plugins/rte/rte.ml
-ML_LINT_KO+=src/plugins/rte/visit.ml
ML_LINT_KO+=src/plugins/scope/Scope.mli
ML_LINT_KO+=src/plugins/scope/datascope.ml
ML_LINT_KO+=src/plugins/scope/defs.ml
diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml
index b6c626b68c4f91251fcdb19397896dc6fec6c40d..e72328ab527209dcb2fb77f130ecc8b50d22e271 100644
--- a/src/plugins/rte/generator.ml
+++ b/src/plugins/rte/generator.ml
@@ -32,26 +32,26 @@ let states : State.t list ref = ref []
let accessors : Db.RteGen.status_accessor list ref = ref []
module Make
- (M:sig
- val name:string
- val parameter: Typed_parameter.t
- val additional_parameters: Typed_parameter.t list
- end)
- =
+ (M:sig
+ val name:string
+ val parameter: Typed_parameter.t
+ val additional_parameters: Typed_parameter.t list
+ end)
+=
struct
- module H =
+ module H =
Kernel_function.Make_Table
(Datatype.Bool)
(struct
- let name = "RTE.Computed." ^ M.name
- let size = 17
- let dependencies =
+ let name = "RTE.Computed." ^ M.name
+ let size = 17
+ let dependencies =
let extract p = State.get p.Typed_parameter.name in
- Ast.self
- :: Options.Trivial.self
- :: List.map extract (M.parameter :: M.additional_parameters)
- end)
+ Ast.self
+ :: Options.Trivial.self
+ :: List.map extract (M.parameter :: M.additional_parameters)
+ end)
let is_computed =
(* Nothing to do for functions without body. *)
@@ -70,42 +70,42 @@ end
module Initialized =
Make
(struct
- let name = "initialized"
- let parameter = Options.DoInitialized.parameter
- let additional_parameters = [ ]
- end)
+ let name = "initialized"
+ let parameter = Options.DoInitialized.parameter
+ let additional_parameters = [ ]
+ end)
module Mem_access =
Make
(struct
- let name = "mem_access"
- let parameter = Options.DoMemAccess.parameter
- let additional_parameters = [ Kernel.SafeArrays.parameter ]
- end)
+ let name = "mem_access"
+ let parameter = Options.DoMemAccess.parameter
+ let additional_parameters = [ Kernel.SafeArrays.parameter ]
+ end)
module Pointer_call =
Make
(struct
- let name = "pointer_call"
- let parameter = Options.DoPointerCall.parameter
- let additional_parameters = []
- end)
+ let name = "pointer_call"
+ let parameter = Options.DoPointerCall.parameter
+ let additional_parameters = []
+ end)
module Div_mod =
Make
(struct
- let name = "division_by_zero"
- let parameter = Options.DoDivMod.parameter
- let additional_parameters = []
- end)
+ let name = "division_by_zero"
+ let parameter = Options.DoDivMod.parameter
+ let additional_parameters = []
+ end)
module Shift =
Make
(struct
- let name = "shift_value_out_of_bounds"
- let parameter = Options.DoShift.parameter
- let additional_parameters = []
- end)
+ let name = "shift_value_out_of_bounds"
+ let parameter = Options.DoShift.parameter
+ let additional_parameters = []
+ end)
module Left_shift_negative =
Make
@@ -126,51 +126,51 @@ module Right_shift_negative =
module Signed_overflow =
Make
(struct
- let name = "signed_overflow"
- let parameter = Kernel.SignedOverflow.parameter
- let additional_parameters = []
- end)
+ let name = "signed_overflow"
+ let parameter = Kernel.SignedOverflow.parameter
+ let additional_parameters = []
+ end)
module Signed_downcast =
Make
(struct
- let name = "downcast"
- let parameter = Kernel.SignedDowncast.parameter
- let additional_parameters = []
- end)
+ let name = "downcast"
+ let parameter = Kernel.SignedDowncast.parameter
+ let additional_parameters = []
+ end)
module Unsigned_overflow =
Make
(struct
- let name = "unsigned_overflow"
- let parameter = Kernel.UnsignedOverflow.parameter
- let additional_parameters = []
- end)
+ let name = "unsigned_overflow"
+ let parameter = Kernel.UnsignedOverflow.parameter
+ let additional_parameters = []
+ end)
module Unsigned_downcast =
Make
(struct
- let name = "unsigned_downcast"
- let parameter = Kernel.UnsignedDowncast.parameter
- let additional_parameters = []
- end)
+ let name = "unsigned_downcast"
+ let parameter = Kernel.UnsignedDowncast.parameter
+ let additional_parameters = []
+ end)
module Float_to_int =
Make
(struct
- let name = "float_to_int"
- let parameter = Options.DoFloatToInt.parameter
- let additional_parameters = []
- end)
+ let name = "float_to_int"
+ let parameter = Options.DoFloatToInt.parameter
+ let additional_parameters = []
+ end)
module Finite_float =
Make
(struct
- let name = "finite_float"
- let parameter = Kernel.SpecialFloat.parameter
- let additional_parameters = []
- end)
+ let name = "finite_float"
+ let parameter = Kernel.SpecialFloat.parameter
+ let additional_parameters = []
+ end)
module Bool_value =
Make
@@ -191,11 +191,11 @@ let () = Db.RteGen.self := self
let all_statuses = !accessors
let emitter =
- Emitter.create
- "rte"
- [ Emitter.Property_status; Emitter.Alarm ]
- ~correctness:[ Kernel.SafeArrays.parameter ]
- ~tuning:[]
+ Emitter.create
+ "rte"
+ [ Emitter.Property_status; Emitter.Alarm ]
+ ~correctness:[ Kernel.SafeArrays.parameter ]
+ ~tuning:[]
(*
Local Variables:
diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 7c646c80c6e977aaf0ae01337b4425641a45e1c1..0b629f7f9941d8f09e6494f4e3c8ca20611539c1 100644
--- a/src/plugins/rte/options.ml
+++ b/src/plugins/rte/options.ml
@@ -21,47 +21,47 @@
(**************************************************************************)
let help_msg = "generates annotations for runtime error checking and \
-preconditions at call sites"
+ preconditions at call sites"
include Plugin.Register
- (struct
- let name = "rtegen"
- let shortname = "rte"
- let help = help_msg
- end)
+ (struct
+ let name = "rtegen"
+ let shortname = "rte"
+ let help = help_msg
+ end)
(* enabling/disabling plugin *)
module Enabled =
False
(struct
- let option_name = "-rte"
- let help = "when on (off by default), " ^ help_msg
- end)
+ let option_name = "-rte"
+ let help = "when on (off by default), " ^ help_msg
+ end)
(* annotates division by zero (undefined behavior) *)
module DoDivMod =
True
(struct
- let option_name = "-rte-div"
- let help = "when on (default), annotate for modulo and division by zero"
- end)
+ let option_name = "-rte-div"
+ let help = "when on (default), annotate for modulo and division by zero"
+ end)
(* annotates left and right shifts (undefined behavior) *)
module DoShift =
True
(struct
- let option_name = "-rte-shift"
- let help = "when on (default), annotate for left and right shifts by a value out of bounds"
- end)
+ let option_name = "-rte-shift"
+ let help = "when on (default), annotate for left and right shifts by a value out of bounds"
+ end)
(* annotates casts from floating-point to integer (undefined behavior) *)
module DoFloatToInt =
True
(struct
- let option_name = "-rte-float-to-int"
- let help = "when on (default), annotate casts from floating-point to \
- integer"
- end)
+ let option_name = "-rte-float-to-int"
+ let help = "when on (default), annotate casts from floating-point to \
+ integer"
+ end)
(* annotates local variables and pointers read (aside from globals) initialization *)
module DoInitialized =
@@ -76,52 +76,52 @@ module DoInitialized =
module DoMemAccess =
True
(struct
- let option_name = "-rte-mem"
- let help = "when on (default), annotate for valid pointer or \
-array access"
- end)
+ let option_name = "-rte-mem"
+ let help = "when on (default), annotate for valid pointer or \
+ array access"
+ end)
(* annotates calls through pointers *)
module DoPointerCall =
True
(struct
- let option_name = "-rte-pointer-call"
- let help = "when on, annotate functions calls through pointers"
- end)
+ let option_name = "-rte-pointer-call"
+ let help = "when on, annotate functions calls through pointers"
+ end)
(* uses results of basic constant propagation in order to check
validity / invalidity of generated assertions, emitting a status if possible
- *)
+*)
module Trivial =
False
(struct
- let option_name = "-rte-trivial-annotations"
- let help = "generate annotations for constant expressions, even when \
-they trivially hold"
- (* if on, evaluates constants in order to check if assertions
- are trivially true / false *)
- end)
+ let option_name = "-rte-trivial-annotations"
+ let help = "generate annotations for constant expressions, even when \
+ they trivially hold"
+ (* if on, evaluates constants in order to check if assertions
+ are trivially true / false *)
+ end)
-(* emits a warning when an assertion generated by rte is clearly invalid
+(* emits a warning when an assertion generated by rte is clearly invalid
(using constant folding, see ConstFold *)
module Warn =
True
(struct
- let option_name = "-rte-warn"
- let help = "when on (default), emits warning on broken asserts"
- end)
+ let option_name = "-rte-warn"
+ let help = "when on (default), emits warning on broken asserts"
+ end)
(* this option allows the user to select a set of functions on which
- the plug-in performs its jobs (and only those).
+ the plug-in performs its jobs (and only those).
By default all functions are annotated *)
module FunctionSelection =
Kernel_function_set
(struct
- let option_name = "-rte-select"
- let arg_name = "fun"
- let help = "select <fun> for analysis (default all functions)"
- end)
-
+ let option_name = "-rte-select"
+ let arg_name = "fun"
+ let help = "select <fun> for analysis (default all functions)"
+ end)
+
let warn ?source fmt = warning ?source ~current:true ~once:true fmt
(*
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 5a7a9ba4af947ea862faa59e349c55e4b3cb1805..8831d66b29bd97f63ed288741c8d83c607594568 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-let journal_register ?comment is_dyn name ty_arg fctref fct =
+let journal_register ?comment is_dyn name ty_arg fctref fct =
let ty = Datatype.func ty_arg Datatype.unit in
Db.register (Db.Journalize("RteGen." ^ name, ty)) fctref fct;
if is_dyn then
@@ -29,21 +29,21 @@ let journal_register ?comment is_dyn name ty_arg fctref fct =
in
()
-let nojournal_register fctref fct =
+let nojournal_register fctref fct =
Db.register Db.Journalization_not_required fctref (fun () -> fct)
-let () =
+let () =
journal_register false
"annotate_kf" Kernel_function.ty Db.RteGen.annotate_kf Visit.annotate_kf;
- journal_register false "compute" Datatype.unit Db.RteGen.compute
+ journal_register false "compute" Datatype.unit Db.RteGen.compute
Visit.compute;
journal_register true
~comment:"Generate all RTE annotations in the \
- given function."
+ given function."
"do_all_rte" Kernel_function.ty Db.RteGen.do_all_rte Visit.do_all_rte;
journal_register false
~comment:"Generate all RTE annotations except pre-conditions \
- in the given function."
+ in the given function."
"do_rte" Kernel_function.ty Db.RteGen.do_rte Visit.do_rte;
let open Generator in
let open Db.RteGen in
@@ -76,7 +76,7 @@ let _ =
let _ =
Dynamic.register
~comment:"Get the list of annotations previously emitted by RTE for the \
-given statement."
+ given statement."
~plugin:"RteGen"
"get_rte_annotations"
(Datatype.func
@@ -88,7 +88,7 @@ given statement."
let _ =
Dynamic.register
~comment:"Generate RTE annotations corresponding to the given stmt of \
-the given function."
+ the given function."
~plugin:"RteGen"
"stmt_annotations"
(Datatype.func2 Kernel_function.ty Cil_datatype.Stmt.ty
@@ -99,10 +99,10 @@ the given function."
let _ =
Dynamic.register
~comment:"Generate RTE annotations corresponding to the given exp \
-of the given stmt in the given function."
+ of the given stmt in the given function."
~plugin:"RteGen"
"exp_annotations"
- (Datatype.func3 Kernel_function.ty Cil_datatype.Stmt.ty Cil_datatype.Exp.ty
+ (Datatype.func3 Kernel_function.ty Cil_datatype.Stmt.ty Cil_datatype.Exp.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
~journalize:false
Visit.do_exp_annotations
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 855e2b4e729349a97a695626041ebe7d19df816c..130ec5506858bfa9a07a75eb8687dc99e86a730f 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -54,7 +54,7 @@ let valid_index ~remove_trivial ~on_alarm e size =
let v_e = get_expr_val e in
let v_size = get_expr_val size in
let neg_ok =
- Extlib.may_map ~dft:false (Integer.le Integer.zero) v_e
+ Extlib.may_map ~dft:false (Integer.le Integer.zero) v_e
|| Cil.isUnsignedInteger (Cil.typeOf e)
in
if not neg_ok then alarm Lower_bound;
@@ -76,10 +76,10 @@ let valid_index ~remove_trivial ~on_alarm e size =
let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
(* For accesses to known arrays we generate an assertions that constrains
the index. This is simpler than the [\valid] assertion *)
- let rec check_array_access default off typ in_struct =
+ let rec check_array_access default off typ in_struct =
match off with
- | NoOffset ->
- if default then
+ | NoOffset ->
+ if default then
on_alarm ?status:None (Alarms.Memory_access(lv, read_only))
| Field (fi, off) ->
(* Mark that we went through a struct field, then recurse *)
@@ -108,10 +108,10 @@ let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
(* assertion for lvalue initialization *)
let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
- let rec check_array_initialized default off typ in_struct l =
+ let rec check_array_initialized default off typ in_struct l =
match off with
- | NoOffset ->
- begin
+ | NoOffset ->
+ begin
match typ with
| TComp({cstruct = false; cfields} ,_,_) ->
(match cfields with
@@ -123,10 +123,10 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
(fun fi -> Cil.addOffsetLval (Field (fi, NoOffset)) lv)
cfields
in
- if default then
+ if default then
on_alarm ?status:None (Alarms.Uninitialized_union llv))
- | _ ->
- if default then
+ | _ ->
+ if default then
on_alarm ?status:None (Alarms.Uninitialized lv)
end
| Field (fi, off) ->
@@ -165,7 +165,7 @@ let uminus_assertion ~remove_trivial ~on_alarm exp =
if remove_trivial then begin
match get_expr_val exp with
| None -> alarm ()
- | Some a64 ->
+ | Some a64 ->
(* constant operand *)
if Integer.equal a64 min_ty then
alarm ~status:Property_status.False_if_reachable ()
@@ -179,9 +179,9 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
is strictly more than [max_ty] or strictly less than [min_ty] *)
let t = Cil.unrollType (Cil.typeOf exp) in
let size = Cil.bitsSizeOf t in
- let min_ty, max_ty =
+ let min_ty, max_ty =
if signed then Cil.min_signed_number size, Cil.max_signed_number size
- else Integer.zero, Cil.max_unsigned_number size
+ else Integer.zero, Cil.max_unsigned_number size
in
let alarm ?status bk =
let bound = match bk with
@@ -228,7 +228,7 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
(* Only negative overflows are possible, since r is positive. (TODO:
nothing can happen on [max_int]. *)
alarm Lower_bound
- end
+ end
| Some v, None, Mult | None, Some v, Mult
when Integer.is_zero v || Integer.is_one v -> ()
@@ -286,7 +286,7 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
| Some _, Some _ ->
(* invalid constant division *)
alarm ~status:Property_status.False_if_reachable ()
- | None, Some _ | Some _, None | None, None ->
+ | None, Some _ | Some _, None | None, None ->
(* at least one is not constant: cannot conclude *)
alarm ()
end
@@ -347,12 +347,12 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
in
if remove_trivial then begin
match get_expr_val lexp, get_expr_val rexp with
- | None,_ | _, None ->
+ | None,_ | _, None ->
overflow_alarm ()
| Some lval64, Some rval64 ->
(* both operands are constant: check result is representable in
result type *)
- if Integer.ge rval64 Integer.zero
+ if Integer.ge rval64 Integer.zero
&& Integer.gt (Integer.shift_left lval64 rval64) maxValResult
then
overflow_alarm ~status:Property_status.False_if_reachable ()
@@ -384,7 +384,7 @@ let unsigned_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
on_alarm ?status a;
in
let alarms () =
- if Cil.isSigned kind then begin (* signed to unsigned *)
+ if Cil.isSigned kind then begin (* signed to unsigned *)
alarm Upper_bound;
alarm Lower_bound;
end else (* unsigned to unsigned; cannot overflow in the negative *)
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index c8091e90c750efa7277e1caec1f71c0451f8906e..19c5fa1fa52b6ce3454abd403feee30c62e01b01 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -28,7 +28,7 @@ open Cil_datatype
(* AST inplace visitor for runtime annotation generation *)
(* module for bypassing categories of annotation generation for certain
- expression ids ;
+ expression ids ;
useful in a case such as
signed char cx,cy,cz;
@@ -177,8 +177,8 @@ class annot_visitor kf to_annot on_alarm = object (self)
let stmt = Extlib.the (self#current_stmt) in
Queue.add
(fun () ->
- let annot = Logic_const.new_code_annotation (AStmtSpec ([], spec)) in
- Annotations.add_code_annot Generator.emitter ~kf stmt annot)
+ let annot = Logic_const.new_code_annotation (AStmtSpec ([], spec)) in
+ Annotations.add_code_annot Generator.emitter ~kf stmt annot)
self#get_filling_actions
method private generate_assertion: 'a. 'a Rte.alarm_gen -> 'a -> unit =
@@ -188,22 +188,22 @@ class annot_visitor kf to_annot on_alarm = object (self)
fgen ~remove_trivial ~on_alarm
method! vstmt s = match s.skind with
- | UnspecifiedSequence l ->
- (* UnspecifiedSequences may contain lvals for side-effects, that
- give rise to spurious assertions *)
- let no_lval = List.map (fun (s, _, _, _, sref) -> s, [], [], [], sref) l in
- let s' = { s with skind = UnspecifiedSequence no_lval } in
- Cil.ChangeDoChildrenPost (s', fun _ -> s)
- | _ -> Cil.DoChildren
+ | UnspecifiedSequence l ->
+ (* UnspecifiedSequences may contain lvals for side-effects, that
+ give rise to spurious assertions *)
+ let no_lval = List.map (fun (s, _, _, _, sref) -> s, [], [], [], sref) l in
+ let s' = { s with skind = UnspecifiedSequence no_lval } in
+ Cil.ChangeDoChildrenPost (s', fun _ -> s)
+ | _ -> Cil.DoChildren
method private treat_call ret_opt =
match ret_opt, self#do_mem_access () with
| None, _ | Some _, false -> ()
- | Some ret, true ->
+ | Some ret, true ->
Options.debug "lval %a: validity of potential mem access checked\n"
- Printer.pp_lval ret;
- self#generate_assertion
- (Rte.lval_assertion ~read_only:Alarms.For_writing) ret
+ Printer.pp_lval ret;
+ self#generate_assertion
+ (Rte.lval_assertion ~read_only:Alarms.For_writing) ret
method private check_uchar_assign dest src =
@@ -215,59 +215,59 @@ class annot_visitor kf to_annot on_alarm = object (self)
dest
end;
begin match src.enode with
- | Lval src_lv ->
- let typ1 = Cil.typeOfLval src_lv in
- let typ2 = Cil.typeOfLval dest in
- let isUChar t = Cil.isUnsignedInteger t && Cil.isAnyCharType t in
- if isUChar typ1 && isUChar typ2 then
- self#mark_to_skip_initialized src_lv
- | _ -> ()
+ | Lval src_lv ->
+ let typ1 = Cil.typeOfLval src_lv in
+ let typ2 = Cil.typeOfLval dest in
+ let isUChar t = Cil.isUnsignedInteger t && Cil.isAnyCharType t in
+ if isUChar typ1 && isUChar typ2 then
+ self#mark_to_skip_initialized src_lv
+ | _ -> ()
end ;
Cil.DoChildren
(* assigned left values are checked for valid access *)
method! vinst = function
- | Set (lval,exp,_) -> self#check_uchar_assign lval exp
- | Call (ret_opt,funcexp,argl,_) ->
- (* Do not emit alarms on Eva builtins such as Frama_C_show_each, that should
- have no effect on analyses. *)
- let is_builtin, is_va_start =
- match funcexp.enode with
- | Lval (Var vinfo, NoOffset) ->
- let kf = Globals.Functions.get vinfo in
- let frama_b = Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
- in
- let va_start = Kernel_function.get_name kf = "__builtin_va_start" in
- (frama_b, va_start)
- | _ -> (false, false)
- in
- if is_va_start then begin
- match (List.nth argl 0).enode with
+ | Set (lval,exp,_) -> self#check_uchar_assign lval exp
+ | Call (ret_opt,funcexp,argl,_) ->
+ (* Do not emit alarms on Eva builtins such as Frama_C_show_each, that should
+ have no effect on analyses. *)
+ let is_builtin, is_va_start =
+ match funcexp.enode with
+ | Lval (Var vinfo, NoOffset) ->
+ let kf = Globals.Functions.get vinfo in
+ let frama_b = Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
+ in
+ let va_start = Kernel_function.get_name kf = "__builtin_va_start" in
+ (frama_b, va_start)
+ | _ -> (false, false)
+ in
+ if is_va_start then begin
+ match (List.nth argl 0).enode with
| Lval lv -> self#mark_to_skip_initialized lv
| _ -> ()
- end ;
- if is_builtin
- then Cil.SkipChildren
- else begin
- self#treat_call ret_opt;
- (* Alarm if the call is through a pointer. Done in DoChildrenPost to get a
- more pleasant ordering of annotations. *)
- let do_ptr () =
- if self#do_pointer_call () then
- match funcexp.enode with
- | Lval (Mem e, _) -> self#generate_assertion Rte.pointer_call (e, argl)
- | _ -> ()
- in
- Cil.DoChildrenPost (fun res -> do_ptr (); res)
- end
- | Local_init (v,ConsInit(f,args,kind),loc) ->
- let do_call lv _e _args _loc = self#treat_call lv in
- Cil.treat_constructor_as_func do_call v f args kind loc;
- Cil.DoChildren
- | Local_init (v,AssignInit (SingleInit exp),_) ->
- self#check_uchar_assign (Cil.var v) exp
- | Local_init (_,AssignInit _,_)
- | Asm _ | Skip _ | Code_annot _ -> Cil.DoChildren
+ end ;
+ if is_builtin
+ then Cil.SkipChildren
+ else begin
+ self#treat_call ret_opt;
+ (* Alarm if the call is through a pointer. Done in DoChildrenPost to get a
+ more pleasant ordering of annotations. *)
+ let do_ptr () =
+ if self#do_pointer_call () then
+ match funcexp.enode with
+ | Lval (Mem e, _) -> self#generate_assertion Rte.pointer_call (e, argl)
+ | _ -> ()
+ in
+ Cil.DoChildrenPost (fun res -> do_ptr (); res)
+ end
+ | Local_init (v,ConsInit(f,args,kind),loc) ->
+ let do_call lv _e _args _loc = self#treat_call lv in
+ Cil.treat_constructor_as_func do_call v f args kind loc;
+ Cil.DoChildren
+ | Local_init (v,AssignInit (SingleInit exp),_) ->
+ self#check_uchar_assign (Cil.var v) exp
+ | Local_init (_,AssignInit _,_)
+ | Asm _ | Skip _ | Code_annot _ -> Cil.DoChildren
method! vexpr exp =
Options.debug "considering exp %a\n" Printer.pp_exp exp;
@@ -281,12 +281,12 @@ class annot_visitor kf to_annot on_alarm = object (self)
let generate () =
match exp.enode with
| BinOp((Div | Mod) as op, lexp, rexp, ty) ->
- (match Cil.unrollType ty with
- | TInt(kind,_) ->
+ (match Cil.unrollType ty with
+ | TInt(kind,_) ->
(* add assertion "divisor not zero" *)
if self#do_div_mod () then
self#generate_assertion Rte.divmod_assertion rexp;
- if self#do_signed_overflow () && op = Div && Cil.isSigned kind then
+ if self#do_signed_overflow () && op = Div && Cil.isSigned kind then
(* treat the special case of signed division overflow
(no signed modulo overflow) *)
self#generate_assertion Rte.signed_div_assertion (exp, lexp, rexp)
@@ -295,7 +295,7 @@ class annot_visitor kf to_annot on_alarm = object (self)
| _ -> ())
| BinOp((Shiftlt | Shiftrt) as op, lexp, rexp,ttype ) ->
- (match Cil.unrollType ttype with
+ (match Cil.unrollType ttype with
| TInt(kind,_) ->
(* 0 <= rexp <= width *)
if self#do_shift () then begin
@@ -320,13 +320,13 @@ class annot_visitor kf to_annot on_alarm = object (self)
| BinOp((PlusA |MinusA | Mult) as op, lexp, rexp, ttype) ->
(* may be skipped if the enclosing expression is a downcast to a signed
type *)
- (match Cil.unrollType ttype with
- | TInt(kind,_) when Cil.isSigned kind ->
+ (match Cil.unrollType ttype with
+ | TInt(kind,_) when Cil.isSigned kind ->
if self#do_signed_overflow () && not (self#must_skip exp) then
self#generate_assertion
(Rte.mult_sub_add_assertion ~signed:true)
(exp, op, lexp, rexp)
- | TInt(kind,_) when not (Cil.isSigned kind) ->
+ | TInt(kind,_) when not (Cil.isSigned kind) ->
if self#do_unsigned_overflow () then
self#generate_assertion
(Rte.mult_sub_add_assertion ~signed:false)
@@ -340,8 +340,8 @@ class annot_visitor kf to_annot on_alarm = object (self)
"subtracting the promoted value from the largest value
of the promoted type and adding one",
the result is always representable: so no overflow *)
- (match Cil.unrollType ty with
- | TInt(kind,_) when Cil.isSigned kind ->
+ (match Cil.unrollType ty with
+ | TInt(kind,_) when Cil.isSigned kind ->
if self#do_signed_overflow () then
self#generate_assertion Rte.uminus_assertion exp;
| TFloat(fkind,_) when self#do_finite_float () ->
@@ -356,9 +356,9 @@ class annot_visitor kf to_annot on_alarm = object (self)
(* left values are checked for valid access *)
if self#do_mem_access () then begin
Options.debug
- "exp %a is an lval: validity of potential mem access checked"
+ "exp %a is an lval: validity of potential mem access checked"
Printer.pp_exp exp;
- self#generate_assertion
+ self#generate_assertion
(Rte.lval_assertion ~read_only:Alarms.For_reading) lval
end;
if self#do_initialized () && not (self#must_skip_initialized lval) then begin
@@ -391,12 +391,12 @@ class annot_visitor kf to_annot on_alarm = object (self)
| _ -> ());
| Const (CReal(f,fkind,_)) when self#do_finite_float () ->
begin match Pervasives.classify_float f with
- | FP_normal
- | FP_subnormal
- | FP_zero -> ()
- | FP_infinite
- | FP_nan ->
- self#generate_assertion Rte.finite_float_assertion (fkind,exp)
+ | FP_normal
+ | FP_subnormal
+ | FP_zero -> ()
+ | FP_infinite
+ | FP_nan ->
+ self#generate_assertion Rte.finite_float_assertion (fkind,exp)
end
| StartOf _
| AddrOf _
@@ -416,7 +416,7 @@ class annot_visitor kf to_annot on_alarm = object (self)
end
-let rte_annotations stmt =
+let rte_annotations stmt =
Annotations.fold_code_annot
(fun e a acc -> if Emitter.equal e Generator.emitter then a ::acc else acc)
stmt