Merge branch 'topic/272-kanig-renaming' into 'master'

Rename units and types in gnatwhy3

Issue: eng/spark/spark2014#272

See merge request eng/spark/why3!67

Makefile.in

@@ -753,7 +753,7 @@ clean::
 ############
 
 GNATWHY3_FILES := gnat_util gnat_loc gnat_expl gnat_counterexamples gnat_config\
-	      gnat_scheduler gnat_manual gnat_report gnat_objectives gnat_main
+	      gnat_scheduler gnat_manual gnat_report gnat_checks gnat_main
 
 GNATWHY3MODULES := $(addprefix src/gnat/, $(GNATWHY3_FILES))
 GNATWHY3DEP = $(addsuffix .dep, $(GNATWHY3MODULES))

src/gnat/gnat_objectives.mli → src/gnat/gnat_checks.mli

@@ -1,65 +1,62 @@
-(* This module is the Database for objectives and goals. It also deals with the
+(* This module is the Database for checks and goals. It also deals with the
    better part of scheduling of VCs.
 
-   An objective is something to be proved in Ada, say, a range check. An
-   objective is defined by an explanation (reason + Ada location).
+   A check is something to be proved in Ada, say, a range check. A
+   check is defined by an explanation (check kind + Ada location). This is the
+   Gnat_expl.check type.
 
    A goal is a VC that will be sent to Alt-Ergo. In general, there will be many
-   goals for each objective. Each goal has a trace (list of locations).
+   goals for each check. Each goal has a trace (list of locations).
 
    This module has the following functionality:
-      - It answers queries to get the goals of an objective and the
-        objective of a goal.
+      - It answers queries to get the goals of a check and the
+        check of a goal.
       - It supports scheduling by providing a "next" function that will by
-      little chunks return all goals associated to an objective.
+      little chunks return all goals associated to a check.
       - It allows registering prover results and keeps track of the status of
-        an objective.
+        a check.
       - It defines the scheduler and initializes it, and all the goals,
         correctly.
 *)
 
 open Why3
 
-type objective = Gnat_expl.check
-(* an objective is identified by its check, which contains the check id and the
-   kind of the check *)
-
 type status =
    | Proved
    | Not_Proved
    | Work_Left
    | Counter_Example
-(* These are the possible statuses of an objective.
-   [Proved] means that all goals of that objectives are proved.
-   [Not_Proved] means that a proof attempt for a goal of the objective that
+(* These are the possible statuses of a check.
+   [Proved] means that all goals of that check are proved.
+   [Not_Proved] means that a proof attempt for a goal of the check that
                cannot (or should not) be further simplified has failed.
 
    In both cases, there is no more work to do, and we can issue a message to
    the user.
 
-   [Work_Left] means that we don't know yet whether the objective is proved or
+   [Work_Left] means that we don't know yet whether the check is proved or
                not, this means that all subgoals were proved up to now or if
                unproved could be further simplified, but there is some work
                left.
-   [Counter_Example] means that the objective cannot be proved and the
+   [Counter_Example] means that the check cannot be proved and the
                counterexample should be generated.
 *)
 
 type subp
-(* An object of type "subp" represents all objectives for a given Ada
+(* An object of type "subp" represents all checks for a given Ada
    subprogram. *)
 
-(* various possibilities to add objectives and goals to the database, and the
+(* various possibilities to add checks and goals to the database, and the
    "interesting" bit *)
 
 type goal_id = Session_itp.proofNodeID
 (* This is the type of identifier of goal. They can be queried from the session
    through Session_itp functions *)
 
-val add_to_objective : Gnat_expl.vc_info -> goal_id -> unit
-(* register the goal with the given objective. If this is the
-   first time we register a goal for given objective, the objective is
-   registered as well. Only do the registering if the objective is to de
+val add_to_check : Gnat_expl.vc_info -> goal_id -> unit
+(* register the goal with the given check. If this is the
+   first time we register a goal for given check, the check is
+   registered as well. Only do the registering if the check is to be
    discharged (ie, if the --limit-subp / --limit-line directives apply). *)
 
 val set_not_interesting : goal_id -> unit
@@ -71,22 +68,22 @@ val is_interesting : goal_id -> bool
 
 val add_trivial_proof : Session_itp.session -> goal_id -> unit
 
-val get_objective : goal_id -> objective
-(* get the objective associated with a goal_id *)
+val get_check_of_goal : goal_id -> Gnat_expl.check
+(* get the check associated with a goal_id *)
 val get_extra_info   : goal_id -> Gnat_expl.extra_info
 
 (* Scheduling and proof *)
-val next : objective -> goal_id list
-(* For an objective, successive calls of [next] will return all goal_ids
-   associated to the objective, by chunks of size Gnat_config.parallel. [] is
-   returned if no goal_ids are left. One can add new goal_ids to an objective at any
+val next : Gnat_expl.check -> goal_id list
+(* For a check, successive calls of [next] will return all goal_ids
+   associated to the check, by chunks of size Gnat_config.parallel. [] is
+   returned if no goal_ids are left. One can add new goal_ids to a check at any
    time. *)
 
 
 (* Auxiliary functions *)
 
-val iter : (objective -> unit) -> unit
-(* iterate over all objectives *)
+val iter : (Gnat_expl.check -> unit) -> unit
+(* iterate over all registered checks *)
 
 val iter_leaf_goals :
     Session_itp.session -> subp ->
@@ -98,10 +95,10 @@ val all_provers_tried : Session_itp.session -> goal_id -> bool
 (* check whether an existing valid proof attempt exists for the goal_id, for all
    requested provers *)
 
-val objective_status : objective -> status
-(* query the status of the objective *)
+val check_status : Gnat_expl.check -> status
+(* query the status of the check *)
 
-val ce_goal : objective -> goal_id option
+val ce_goal : Gnat_expl.check -> goal_id option
 
 val init_cont : unit -> Controller_itp.controller
 (* Makes a new controller with session *)
@@ -127,9 +124,9 @@ end
 
 module Make (S: Controller_itp.Scheduler) : sig
 
-val register_result : Controller_itp.controller -> goal_id -> bool -> objective * status
+val register_result : Controller_itp.controller -> goal_id -> bool -> Gnat_expl.check * status
 (* Register the result of a prover for a given goal_id, and return the updated
- * status of the objective, as well as the objective itself *)
+ * status of the check, as well as the check itself *)
 
 val schedule_goal :
     callback:(Session_itp.proofAttemptID -> Controller_itp.proof_attempt_status -> unit) ->
@@ -162,14 +159,14 @@ module Save_VCs : sig
    (* Provide saving of VCs, traces *)
 
    val extract_stats :
-     Controller_itp.controller -> objective -> Gnat_report.stats * int
+     Controller_itp.controller -> Gnat_expl.check -> Gnat_report.stats * int
    (* The second field of the return tuple is the number of goal proved by a
       transformation that is not trivial_true (Checker prover). *)
 
    val vc_file : goal_id -> string
    (* get the file name for a given goal *)
 
-   val check_to_json : Session_itp.session -> objective -> Json_base.json
+   val check_to_json : Session_itp.session -> Gnat_expl.check -> Json_base.json
 end
 
 val all_split_leaf_goals : unit -> unit
@@ -181,8 +178,8 @@ val goal_has_splits : Session_itp.session -> goal_id -> bool
 val is_ce_goal : Session_itp.session -> Session_itp.proofNodeID -> bool
 val is_valid_not_ce: Session_itp.session -> Session_itp.proofNodeID -> bool
 
-val session_proved_status : Controller_itp.controller -> objective -> bool
-(* check the proof status of an objective by looking at the verified/not
+val session_proved_status : Controller_itp.controller -> Gnat_expl.check -> bool
+(* check the proof status of an check by looking at the verified/not
    verified status of its VCs in the session *)
 
 val remove_all_valid_ce_attempt: Session_itp.session -> unit
@@ -191,17 +188,17 @@ val remove_all_valid_ce_attempt: Session_itp.session -> unit
    or try greater timeout ? *)
 
 val session_find_unproved_pa :
-    Controller_itp.controller -> objective -> Session_itp.proofAttemptID option
+    Controller_itp.controller -> Gnat_expl.check -> Session_itp.proofAttemptID option
 (* find the first unproved (not obsolete) proof attempt in a session which is
- *  in subforest of objective. *)
+ *  in subforest of check. *)
 
 val session_find_ce_pa :
-    Controller_itp.controller -> objective -> Session_itp.proofAttemptID option
+    Controller_itp.controller -> Gnat_expl.check -> Session_itp.proofAttemptID option
 (* Find the proof attempt related to the counter example, if any *)
 
 val session_find_unproved_goal :
-    Controller_itp.controller -> objective -> Session_itp.proofNodeID option
-(* find the first unproved goal in a session (in subforest of objective) *)
+    Controller_itp.controller -> Gnat_expl.check -> Session_itp.proofNodeID option
+(* find the first unproved goal in a session (in subforest of check) *)
 
 
 val replay : Controller_itp.controller -> unit

src/gnat/gnat_expl.ml

@@ -1,7 +1,7 @@
 open Why3
 open Term
 
-type reason =
+type check_kind =
    (* VC_RTE_Kind - run-time checks *)
    | VC_Division_Check
    | VC_Index_Check
@@ -67,7 +67,7 @@ type reason =
    | VC_Unreachable_Branch
    | VC_Dead_Code
 
-let is_warning_reason r =
+let is_warning_kind r =
   match r with
    (* VC_RTE_Kind - run-time checks *)
    | VC_Division_Check
@@ -141,7 +141,7 @@ type subp_entity = Gnat_loc.loc
 type id = int
 type check =
   { id             : id;
-    reason         : reason;
+    check_kind     : check_kind;
     sloc           : Gnat_loc.loc;
     shape          : string;
     already_proved : bool
@@ -168,20 +168,20 @@ type limit_mode =
 let check_compare a b =
   let c = Stdlib.compare a.id b.id in
   if c <> 0 then c
-  else Stdlib.compare a.reason b.reason
+  else Stdlib.compare a.check_kind b.check_kind
 
 let check_equal a b =
-  Stdlib.(=) a.id b.id && Stdlib.(=) a.reason b.reason
+  Stdlib.(=) a.id b.id && Stdlib.(=) a.check_kind b.check_kind
 
-let check_hash e = Hashcons.combine (Hashtbl.hash e.id) (Hashtbl.hash e.reason)
+let check_hash e = Hashcons.combine (Hashtbl.hash e.id) (Hashtbl.hash e.check_kind)
 
-let mk_check ?shape:shape reason id sloc ap =
-  { reason = reason; id = id ; sloc = sloc ; already_proved = ap;
+let mk_check ?shape:shape check_kind id sloc ap =
+  { check_kind = check_kind; id = id ; sloc = sloc ; already_proved = ap;
     shape = match shape with None -> "" | Some s -> s }
 
 let get_loc c = c.sloc
-let get_reason c = c.reason
-let reason_from_string s =
+let get_check_kind c = c.check_kind
+let check_kind_from_string s =
    match s with
    (* VC_RTE_Kind - run-time checks *)
    | "VC_DIVISION_CHECK"            -> VC_Division_Check
@@ -250,11 +250,11 @@ let reason_from_string s =
    | "VC_UNREACHABLE_BRANCH"        -> VC_Unreachable_Branch
    | "VC_DEAD_CODE"                 -> VC_Dead_Code
    | _                              ->
-       let s = Format.sprintf "unknown VC reason: %s@." s in
+       let s = Format.sprintf "unknown VC kind: %s@." s in
        Gnat_util.abort_with_message ~internal:true s
 
-let reason_to_ada reason =
-   match reason with
+let check_kind_to_ada kind =
+   match kind with
    (* VC_RTE_Kind - run-time checks *)
    | VC_Division_Check            -> "VC_DIVISION_CHECK"
    | VC_Index_Check               -> "VC_INDEX_CHECK"
@@ -322,8 +322,8 @@ let reason_to_ada reason =
    | VC_Unreachable_Branch        -> "VC_UNREACHABLE_BRANCH"
    | VC_Dead_Code                 -> "VC_DEAD_CODE"
 
-let reason_to_string reason =
-   match reason with
+let check_kind_to_string kind =
+   match kind with
    (* VC_RTE_Kind - run-time checks *)
    | VC_Division_Check            -> "division_check"
    | VC_Index_Check               -> "index_check"
@@ -390,17 +390,17 @@ let reason_to_string reason =
    | VC_Dead_Code                 -> "dead_code"
 
 type gp_label =
-  | Gp_Check of int * reason * Gnat_loc.loc
+  | Gp_Check of int * check_kind * Gnat_loc.loc
   | Gp_Pretty_Ada of int
   | Gp_Shape of string
   | Gp_Already_Proved
   | Gp_Inlined
 
 let parse_check_string s l =
   match l with
-  | id::reason_string::sloc_rest ->
+  | id::check_kind_string::sloc_rest ->
     begin try
-      Gp_Check (int_of_string id, reason_from_string reason_string, Gnat_loc.parse_loc sloc_rest)
+      Gp_Check (int_of_string id, check_kind_from_string check_kind_string, Gnat_loc.parse_loc sloc_rest)
     with e when Debug.test_flag Debug.stack_trace -> raise e
     | Failure _ ->
        let s =
@@ -447,7 +447,7 @@ let read_label s =
 
 type my_expl =
    { mutable check_id       : int option;
-     mutable check_reason   : reason option;
+     mutable check_kind     : check_kind option;
      mutable extra_node     : int option;
      mutable check_sloc     : Gnat_loc.loc option;
      mutable shape          : string option;
@@ -459,13 +459,14 @@ type my_expl =
 
 let default_expl =
    { check_id       = None;
-     check_reason   = None;
+     check_kind     = None;
      check_sloc     = None;
      extra_node     = None;
      shape          = None;
      already_proved = false;
      inline         = None;
    }
+
 let read_vc_labels acc s =
    (* This function takes a set of labels and extracts a "node_info" from that
       set. We start with an empty record; We fill it up by iterating over all
@@ -475,8 +476,8 @@ let read_vc_labels acc s =
      (fun x ->
         let s = x.Ident.attr_string in
         match read_label s with
-        | Some Gp_Check (id, reason, sloc) ->
-            b.check_reason <- Some reason;
+        | Some Gp_Check (id, kind, sloc) ->
+            b.check_kind <- Some kind;
             b.check_id <- Some id;
             b.check_sloc <- Some sloc;
         | Some Gp_Pretty_Ada node ->
@@ -493,26 +494,26 @@ let read_vc_labels acc s =
      ) s;
      (* We potentially need to rectify in the case of loop invariants: We need
         to check whether the VC is for initialization or preservation *)
-     if b.check_reason = Some VC_Loop_Invariant then begin
+     if b.check_kind = Some VC_Loop_Invariant then begin
         Ident.Sattr.iter (fun x ->
            let s = x.Ident.attr_string in
            if Strings.has_prefix "expl:" s then
               if s = "expl:loop invariant init" then
-                 b.check_reason <- Some VC_Loop_Invariant_Init
+                 b.check_kind <- Some VC_Loop_Invariant_Init
               else
-                 b.check_reason <- Some VC_Loop_Invariant_Preserv) s
+                 b.check_kind <- Some VC_Loop_Invariant_Preserv) s
      end;
      b
 
 (* Transform an object of my_expl type into a check *)
 let extract_check b =
      match b with
      | { check_id = Some id ;
-         check_reason = Some reason;
+         check_kind = Some check_kind;
          check_sloc = Some sloc;
          shape = shape;
          already_proved = ap; } ->
-           Some (mk_check ?shape reason id sloc ap)
+           Some (mk_check ?shape check_kind id sloc ap)
      | _ -> None
 
 (* Copied from Termcode and modified to use an accumulator. Traverse the
@@ -550,7 +551,7 @@ let to_filename fmt check =
       let file, line, col = Gnat_loc.explode x in
       Format.fprintf fmt "%s_%d_%d_" file line col;
   ) check.sloc;
-  Format.fprintf fmt "%s" (reason_to_string check.reason)
+  Format.fprintf fmt "%s" (check_kind_to_string check.check_kind)
 
 let parse_line_spec s =
    try
@@ -565,7 +566,7 @@ let parse_line_spec s =
      | [fn;line;col;check] ->
          let line = int_of_string line in
          let col = int_of_string col in
-         let check = reason_from_string check in
+         let check = check_kind_from_string check in
          let loc = Gnat_loc.mk_loc fn line col None in
          Limit_Check (mk_check check 0 loc false)
      | _ ->