new debug flag print_locs to display source locations

src/core/pretty.ml

@@ -28,6 +28,7 @@ open Theory
 open Task
 
 let debug_print_labels = Debug.register_flag "print_labels"
+let debug_print_locs = Debug.register_flag "print_locs"
 
 let iprinter,tprinter,pprinter =
   let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
@@ -190,11 +191,19 @@ let prio_binop = function
 let print_label fmt l =
   if l = "" then () else fprintf fmt "\"%s\"" l
 
+let print_loc fmt l =
+  let (f,l,b,e) = Loc.get l in
+  fprintf fmt "#\"%s\" %d %d %d#" f l b e
+
 let print_ident_labels fmt id =
   if Debug.test_flag debug_print_labels && id.id_label <> []
   then fprintf fmt " %a" (print_list space print_label) id.id_label
+  else ();
+  if Debug.test_flag debug_print_locs then
+    Util.option_iter (fun l -> fprintf fmt " %a" print_loc l) id.id_loc
   else ()
 
+
 let rec print_term fmt t = print_lterm 0 fmt t
 
 and print_lterm pri fmt t = match t.t_label with

src/ide/gconfig.ml

@@ -35,6 +35,7 @@ type t =
       mutable max_running_processes : int;
       mutable default_editor : string;
       mutable show_labels : bool;
+      mutable show_locs : bool;
       mutable saving_policy : int;
         (** 0 = always, 1 = never, 2 = ask *)
       mutable env : Env.env;
@@ -97,7 +98,8 @@ let load_config config =
     saving_policy = ide.ide_saving_policy ;
     max_running_processes = Whyconf.running_provers_max main;
     default_editor = ide.ide_default_editor;
-    show_labels = false;
+    show_labels    = false;
+    show_locs      = false;
     config         = config;
     env            = env
   }
@@ -326,6 +328,11 @@ let set_labels_flag =
   fun b ->
     (if b then Debug.set_flag else Debug.unset_flag) fl
 
+let set_locs_flag =
+  let fl = Debug.lookup_flag "print_locs" in
+  fun b ->
+    (if b then Debug.set_flag else Debug.unset_flag) fl
+
 let preferences c =
   let dialog = GWindow.dialog ~title:"Why3: preferences" () in
   let vbox = dialog#vbox in
@@ -415,6 +422,16 @@ let preferences c =
       (fun () -> c.show_labels <- not c.show_labels;
          set_labels_flag c.show_labels)
   in
+  let showlocs =
+    GButton.check_button ~label:"show source locations in formulas"
+      ~packing:display_options_box#add ()
+      ~active:(set_locs_flag c.show_locs;c.show_locs)
+  in
+  let (_ : GtkSignal.id) =
+    showlocs#connect#toggled ~callback:
+      (fun () -> c.show_locs <- not c.show_locs;
+         set_locs_flag c.show_locs)
+  in
   let set_saving_policy n () = c.saving_policy <- n in
 (*
   let label3 = GMisc.label ~text:"IDE" () in

src/ide/gconfig.mli

@@ -30,6 +30,7 @@ type t =
       mutable max_running_processes : int;
       mutable default_editor : string;
       mutable show_labels : bool;
+      mutable show_locs : bool;
       mutable saving_policy : int;
       mutable env : Why3.Env.env;
       mutable config : Whyconf.config;

tests/my_cosine.c

+/*@ lemma method_error: \forall real x;
+  @     \abs(x) <= 0x1p-5 ==> \abs(1.0 - x*x*0.5 - \cos(x)) <= 0x1p-24;
+  @*/
+
+/*@ requires \abs(x) <= 0x1p-5;
+  @ ensures \abs(\result - \cos(x)) <= 0x1p-23;
+  @*/
+float my_cos1(float x) {
+  //@ assert \abs(1.0 - x*x*0.5 - \cos(x)) <= 0x1p-24;
+  return 1.0f - x * x * 0.5f;
+}
+

tests/my_cosine.mlw

+module M
+
+  use import real.RealInfix
+  use import real.Abs
+  use import real.Trigonometry
+  use import floating_point.Rounding
+  use import floating_point.Single
+
+val single_of_real_exact : x:real ->
+  { }
+  single
+  { value result = x }
+
+val add : x:single -> y:single ->
+  { no_overflow NearestTiesToEven ((value x) +. (value y)) }
+  single
+  { value result = round NearestTiesToEven ((value x) +. (value y))}
+
+val sub : x:single -> y:single ->
+  { no_overflow NearestTiesToEven ((value x) -. (value y)) }
+  single
+  { value result = round NearestTiesToEven ((value x) -. (value y))}
+
+val mul : x:single -> y:single ->
+  { no_overflow NearestTiesToEven ((value x) *. (value y)) }
+  single
+  { value result = round NearestTiesToEven ((value x) *. (value y))}
+
+
+lemma method_error
+    "expl:user lemma"
+    #"my_cosine.c" 1 1 100#
+    :
+    "expl:user lemma, the formula"
+    #"my_cosine.c" 1 24 80#
+    forall x:real.
+    abs x  <=. 0x1p-5 -> abs (1.0 -. x*.x*.0.5 -. cos x) <=. 0x1p-24
+  
+let my_cosine (x:single) : single =
+{ abs (value x) <=. 0x1p-5 }
+  assert {
+    "expl:user assertion"
+    #"my_cosine.c" 9 13 53#
+    abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
+  };
+  ("expl:check FP overflow for -"
+   #"my_cosine.c" 10 9 28#
+  sub (single_of_real_exact 1.0)
+      ("expl:check FP overflow for *"
+       #"my_cosine.c" 10 16 28#
+       mul("expl:check FP overflow for *"
+           #"my_cosine.c" 10 16 21#
+           mul x x) (single_of_real_exact 0.5)))
+{ "expl:post-condition"
+  #"my_cosine.c" 7 12 46#
+  abs (value result -. cos (value x)) <=. 0x1p-23 }
+
+end
+
+(*
+Local Variables:
+compile-command: "../../bin/why3ide.byte my_cosine.mlw"
+End:
+*)