Merge branch 'feature/andre/semantic-locations' into 'master'

[Kernel] add functions for semantic comparisons between locations

See merge request frama-c/frama-c!2437

src/kernel_services/ast_queries/cil_datatype.ml

@@ -214,10 +214,23 @@ module Location = struct
     else
       Format.fprintf fmt "generated"
 
+  let pretty_debug fmt loc =
+    Format.fprintf fmt "(%a:%d:%d,%a:%d:%d)"
+      Datatype.Filepath.pretty (fst loc).Filepath.pos_path
+      (fst loc).Filepath.pos_lnum (fst loc).Filepath.pos_cnum
+      Datatype.Filepath.pretty (snd loc).Filepath.pos_path
+      (snd loc).Filepath.pos_lnum (snd loc).Filepath.pos_cnum
+
   let of_lexing_loc (pos1, pos2) =
     Position.of_lexing_pos pos1, Position.of_lexing_pos pos2
   let to_lexing_loc (pos1, pos2) =
     Position.to_lexing_pos pos1, Position.to_lexing_pos pos2
+
+  let equal_start_semantic (pos1, _) (pos2, _) =
+    Filepath.(Datatype.Filepath.equal pos1.pos_path pos2.pos_path
+              && pos1.pos_lnum = pos2.pos_lnum
+              && pos1.pos_cnum - pos1.pos_bol = pos2.pos_cnum - pos2.pos_bol)
+
 end
 
 module Instr = struct

src/kernel_services/ast_queries/cil_datatype.mli

@@ -69,9 +69,26 @@ module Location: sig
         the full-path to the file. The default pretty-printer [pretty] echoes
         [<dir/f>:<l>] *)
   val pretty_line: t Pretty_utils.formatter
+
+  (** Pretty-print both location start and end, including file, line and
+      character offset.
+
+      @since Frama-C+dev
+   *)
+  val pretty_debug: t Pretty_utils.formatter
+
   (** Prints only the line of the location *)
   val of_lexing_loc : Lexing.position * Lexing.position -> t
   val to_lexing_loc : t -> Lexing.position * Lexing.position
+
+  (** Compares two locations semantically, only taking into account their
+      starting position. Compares normalized filenames, lines and columns,
+      but no absolute character offsets.
+
+      @since Frama-C+dev
+   *)
+  val equal_start_semantic : location -> location -> bool
+
 end
 
 module Localisation: Datatype.S with type t = localisation