Commit d5091e6c authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[rte] moving flags and more exports

parent 687f1bf2
......@@ -957,7 +957,7 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
PLUGIN_ENABLE:=$(ENABLE_RTEGEN)
PLUGIN_NAME:=RteGen
PLUGIN_DIR:=src/plugins/rte
PLUGIN_CMO:= options generator rte visit register
PLUGIN_CMO:= options generator rte flags visit register
PLUGIN_DISTRIBUTED:=yes
PLUGIN_INTERNAL_TEST:=yes
PLUGIN_TESTS_DIRS:=rte rte_manual
......
......@@ -1002,6 +1002,8 @@ src/plugins/report/report_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/scan.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/scan.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/RteGen.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/flags.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/flags.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/generator.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/generator.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/options.ml: CEA_LGPL_OR_PROPRIETARY
......
......@@ -20,7 +20,32 @@
(* *)
(**************************************************************************)
(** Some functions are also registered in {!Db.Value}. *)
(** Consult internal plug-in documentation for more details *)
(** Flags for filtering Alarms *)
module Flags : module type of Flags
(** RTE Generator Status & Emitters *)
module Generator : module type of Generator
(** Visitors to iterate over Alarms and/or generate Code-Annotations *)
module Visit : module type of Visit
module Visit : sig
open Cil_types
val annotate_kf: kernel_function -> unit
val do_all_rte: kernel_function -> unit
val do_rte: kernel_function -> unit
val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
val compute: unit -> unit
type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
type 'a iterator = ?flags:Flags.t -> on_alarm ->
Kernel_function.t -> Cil_types.stmt -> 'a -> unit
val iter_lval : lval iterator
val iter_exp : exp iterator
val iter_instr : instr iterator
val iter_stmt : stmt iterator
val annotation :
Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
code_annotation * bool
val register : Emitter.t -> on_alarm
end
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2019 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Fine Tuning Visitors --- *)
(* -------------------------------------------------------------------------- *)
type t = {
remove_trivial: bool;
initialized: bool;
mem_access: bool;
div_mod: bool;
shift: bool;
left_shift_negative: bool;
right_shift_negative: bool;
signed_overflow: bool;
unsigned_overflow: bool;
signed_downcast: bool;
unsigned_downcast: bool;
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
bool_value: bool;
}
let all = {
remove_trivial = true;
initialized = true;
mem_access = true;
div_mod = true;
shift = true;
left_shift_negative = true;
right_shift_negative = true;
signed_overflow = true;
unsigned_overflow = true;
signed_downcast = true;
unsigned_downcast = true;
float_to_int = true;
finite_float = true;
pointer_call = true;
bool_value = true;
}
let none = {
remove_trivial = false;
initialized = false;
mem_access = false;
div_mod = false;
shift = false;
left_shift_negative = false;
right_shift_negative = false;
signed_overflow = false;
unsigned_overflow = false;
signed_downcast = false;
unsigned_downcast = false;
float_to_int = false;
finite_float = false;
pointer_call = false;
bool_value = false;
}
(* Which annotations should be added,
from local options, or deduced from the options of RTE and the kernel *)
let option (get : unit -> bool) = function None -> get () | Some flag -> flag
let default
?remove_trivial
?initialized
?mem_access
?div_mod
?shift
?left_shift_negative
?right_shift_negative
?signed_overflow
?unsigned_overflow
?signed_downcast
?unsigned_downcast
?float_to_int
?finite_float
?pointer_call
?bool_value
() =
{
remove_trivial = option (fun () -> not (Options.Trivial.get ())) remove_trivial ;
initialized = option Options.DoInitialized.get initialized ;
mem_access = option Options.DoMemAccess.get mem_access ;
div_mod = option Options.DoDivMod.get div_mod ;
shift = option Options.DoShift.get shift;
left_shift_negative = option Kernel.LeftShiftNegative.get left_shift_negative ;
right_shift_negative = option Kernel.RightShiftNegative.get right_shift_negative ;
signed_overflow = option Kernel.SignedOverflow.get signed_overflow ;
unsigned_overflow = option Kernel.UnsignedOverflow.get unsigned_overflow ;
signed_downcast = option Kernel.SignedDowncast.get signed_downcast ;
unsigned_downcast = option Kernel.UnsignedDowncast.get unsigned_downcast ;
float_to_int = option Options.DoFloatToInt.get float_to_int ;
finite_float = option (fun () -> Kernel.SpecialFloat.get () <> "none") finite_float ;
pointer_call = option Options.DoPointerCall.get pointer_call ;
bool_value = option Kernel.InvalidBool.get bool_value ;
}
(* -------------------------------------------------------------------------- *)
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2019 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(** Filtering Categories of Alarms *)
(* -------------------------------------------------------------------------- *)
(** Flags for controling the low-level API. Each flag control whether
a category of alarms will be visited or not. *)
type t = {
remove_trivial: bool;
initialized: bool;
mem_access: bool;
div_mod: bool;
shift: bool;
left_shift_negative: bool;
right_shift_negative: bool;
signed_overflow: bool;
unsigned_overflow: bool;
signed_downcast: bool;
unsigned_downcast: bool;
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
bool_value: bool;
}
(** Defaults flags are taken from the Kernel and RTE plug-in options. *)
val default :
?remove_trivial:bool ->
?initialized:bool ->
?mem_access:bool ->
?div_mod:bool ->
?shift:bool ->
?left_shift_negative:bool ->
?right_shift_negative:bool ->
?signed_overflow:bool ->
?unsigned_overflow:bool ->
?signed_downcast:bool ->
?unsigned_downcast:bool ->
?float_to_int:bool ->
?finite_float:bool ->
?pointer_call:bool ->
?bool_value:bool ->
unit -> t
(** All flags set to [true]. *)
val all : t
(** All flags set to [false]. *)
val none : t
(* -------------------------------------------------------------------------- *)
......@@ -24,128 +24,10 @@
open Cil_types
open Cil_datatype
open Flags
(* AST inplace visitor for runtime annotation generation *)
(* module for bypassing categories of annotation generation for certain
expression ids ;
useful in a case such as
signed char cx,cy,cz;
cz = cx * cy;
which translates to
cz = (signed char) ((int) cx * (int) cz) ;
which would in this case be annotated both by
assert
(((int )cx+(int )cy <= 2147483647) and
((int )cx+(int )cy >= (-0x7FFFFFFF-1)));
and
assert (((int )cx+(int )cy <= 127) and ((int )cx+(int )cy >= -128));
while we only want to keep the second assert (comes from the cast,
and is stronger)
*)
type flags = {
remove_trivial: bool;
initialized: bool;
mem_access: bool;
div_mod: bool;
shift: bool;
left_shift_negative: bool;
right_shift_negative: bool;
signed_overflow: bool;
unsigned_overflow: bool;
signed_downcast: bool;
unsigned_downcast: bool;
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
bool_value: bool;
}
let flags_all = {
remove_trivial = true;
initialized = true;
mem_access = true;
div_mod = true;
shift = true;
left_shift_negative = true;
right_shift_negative = true;
signed_overflow = true;
unsigned_overflow = true;
signed_downcast = true;
unsigned_downcast = true;
float_to_int = true;
finite_float = true;
pointer_call = true;
bool_value = true;
}
let flags_none = {
remove_trivial = false;
initialized = false;
mem_access = false;
div_mod = false;
shift = false;
left_shift_negative = false;
right_shift_negative = false;
signed_overflow = false;
unsigned_overflow = false;
signed_downcast = false;
unsigned_downcast = false;
float_to_int = false;
finite_float = false;
pointer_call = false;
bool_value = false;
}
(* Which annotations should be added,
from local options, or deduced from the options of RTE and the kernel *)
let option (get : unit -> bool) = function None -> get () | Some flag -> flag
let default
?remove_trivial
?initialized
?mem_access
?div_mod
?shift
?left_shift_negative
?right_shift_negative
?signed_overflow
?unsigned_overflow
?signed_downcast
?unsigned_downcast
?float_to_int
?finite_float
?pointer_call
?bool_value
() =
{
remove_trivial = option (fun () -> not (Options.Trivial.get ())) remove_trivial ;
initialized = option Options.DoInitialized.get initialized ;
mem_access = option Options.DoMemAccess.get mem_access ;
div_mod = option Options.DoDivMod.get div_mod ;
shift = option Options.DoShift.get shift;
left_shift_negative = option Kernel.LeftShiftNegative.get left_shift_negative ;
right_shift_negative = option Kernel.RightShiftNegative.get right_shift_negative ;
signed_overflow = option Kernel.SignedOverflow.get signed_overflow ;
unsigned_overflow = option Kernel.UnsignedOverflow.get unsigned_overflow ;
signed_downcast = option Kernel.SignedDowncast.get signed_downcast ;
unsigned_downcast = option Kernel.UnsignedDowncast.get unsigned_downcast ;
float_to_int = option Options.DoFloatToInt.get float_to_int ;
finite_float = option (fun () -> Kernel.SpecialFloat.get () <> "none") finite_float ;
pointer_call = option Options.DoPointerCall.get pointer_call ;
bool_value = option Kernel.InvalidBool.get bool_value ;
}
(** [kf]: function to annotate
[flags]: which RTE to generate.
[register]: the action to perform on each RTE alarm *)
......@@ -472,7 +354,7 @@ let iter_alarms visit ?flags (on_alarm:on_alarm) kf stmt element =
ignore (visit (visitor :> Cil.cilVisitor) element)
type 'a iterator =
?flags:flags -> on_alarm ->
?flags:Flags.t -> on_alarm ->
Kernel_function.t -> Cil_types.stmt -> 'a -> unit
let iter_lval : lval iterator = iter_alarms Cil.visitCilLval
......@@ -573,7 +455,7 @@ let annotate_kf kf = annotate_kf_aux (default ()) kf
function *)
let do_all_rte kf =
let flags =
{ flags_all with
{ Flags.all with
signed_downcast = false;
unsigned_downcast = false; }
in
......@@ -583,7 +465,7 @@ let do_all_rte kf =
function *)
let do_rte kf =
let flags =
{ flags_all with
{ Flags.all with
unsigned_overflow = false;
signed_downcast = false;
unsigned_downcast = false; }
......
......@@ -49,53 +49,6 @@ val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
*)
val compute: unit -> unit
(** {2 Low Level Iterator Control} *)
(** Flags for controling the low-level API. Each flag control whether
a category of alarms will be visited or not. *)
type flags = {
remove_trivial: bool;
initialized: bool;
mem_access: bool;
div_mod: bool;
shift: bool;
left_shift_negative: bool;
right_shift_negative: bool;
signed_overflow: bool;
unsigned_overflow: bool;
signed_downcast: bool;
unsigned_downcast: bool;
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
bool_value: bool;
}
(** Defaults flags are taken from the Kernel and RTE plug-in options. *)
val default :
?remove_trivial:bool ->
?initialized:bool ->
?mem_access:bool ->
?div_mod:bool ->
?shift:bool ->
?left_shift_negative:bool ->
?right_shift_negative:bool ->
?signed_overflow:bool ->
?unsigned_overflow:bool ->
?signed_downcast:bool ->
?unsigned_downcast:bool ->
?float_to_int:bool ->
?finite_float:bool ->
?pointer_call:bool ->
?bool_value:bool ->
unit -> flags
(** All flags set to [true]. *)
val flags_all : flags
(** All flags set to [false]. *)
val flags_none : flags
(** {2 Low-Level RTE Iterators}
RTE Iterators allow to traverse a Cil AST fragment (stmt, expr, l-value)
......@@ -120,8 +73,7 @@ val flags_none : flags
type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
(** Type of low-level iterators visiting an element ['a] of the AST *)
type 'a iterator =
?flags:flags -> on_alarm ->
type 'a iterator = ?flags:Flags.t -> on_alarm ->
Kernel_function.t -> Cil_types.stmt -> 'a -> unit
val iter_lval : lval iterator
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment