From f8ff9b022487aba1078aae402c05113d13a04a82 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 14 Sep 2021 15:59:27 +0200
Subject: [PATCH] [printer] slightly more coherent decisions on whether being
verbose or not.
Some more refactoring might not be totally useless
---
src/kernel_internals/runtime/boot.ml | 1 -
src/kernel_services/ast_printing/cil_printer.ml | 17 +++++++++--------
src/kernel_services/ast_printing/printer.ml | 1 -
tests/pdg/oracle/dyn_dpds.res.oracle | 3 +++
.../oracle/check_builtin_bts1440.res.oracle | 10 ++++++++--
5 files changed, 20 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/runtime/boot.ml b/src/kernel_internals/runtime/boot.ml
index 76bd3467780..5a0ecd8ab3f 100644
--- a/src/kernel_internals/runtime/boot.ml
+++ b/src/kernel_internals/runtime/boot.ml
@@ -59,7 +59,6 @@ let () = Db.Main.play := play_analysis
(* Main: let's go! *)
let () =
- Cil_printer.state.Printer_api.print_cil_as_is <- Kernel.debug_atleast 1;
Sys.catch_break true;
let f () =
ignore (Project.create "default");
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 7ca79d3e27a..2afe7bfc31f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -522,7 +522,15 @@ class cil_printer () = object (self)
val mutable logic_printer_enabled = true
- method reset () = ()
+ val mutable verbose = false
+ (* Do not add a value that depends on a
+ non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
+ to the way the pretty-printing class is instantiated, this value would be
+ evaluated too soon. Override the [reset] method instead. *)
+
+ method reset () =
+ verbose <- Kernel.debug_atleast 1;
+ state.print_cil_as_is <- Kernel.debug_atleast 1 || Kernel.PrintAsIs.get()
method pp_keyword fmt s = pp_print_string fmt s
method pp_acsl_keyword = self#pp_keyword
@@ -546,12 +554,6 @@ class cil_printer () = object (self)
(if block then Pretty_utils.pp_close_block else Format.fprintf)
fmt "%(%)" suf
- val mutable verbose = false
- (* Do not add a value that depends on a
- non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
- to the way the pretty-printing class is instantiated, this value would be
- evaluated too soon. Override the [reset] method instead. *)
-
(* indicates whether we are printing ghost elements *)
val mutable is_ghost = false
method private display_comment () = not is_ghost || verbose
@@ -3406,7 +3408,6 @@ class cil_printer () = object (self)
method file fmt file =
fprintf fmt "@[/* Generated by Frama-C */@\n" ;
- state.print_cil_as_is <- state.print_cil_as_is || Kernel.PrintAsIs.get ();
print_std_includes fmt file.globals;
Cil.iterGlobals file (fun g -> self#global fmt g);
fprintf fmt "@]@."
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index c8e1bac0d46..aa74c0cc535 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -96,7 +96,6 @@ class printer_with_annot () = object (self)
method! reset () =
super#reset ();
- verbose <- Kernel.debug_atleast 1;
declared_globs <- Cil_datatype.Varinfo.Set.empty;
print_spec <- false
diff --git a/tests/pdg/oracle/dyn_dpds.res.oracle b/tests/pdg/oracle/dyn_dpds.res.oracle
index 658d717167d..7a8f17e711a 100644
--- a/tests/pdg/oracle/dyn_dpds.res.oracle
+++ b/tests/pdg/oracle/dyn_dpds.res.oracle
@@ -40,6 +40,9 @@ int main(int a, int b, int c)
x = - x;
/* sid:6 */
/*@ assert *p > G; */ ;
+ }
+ else {
+
}
/* sid:9 */
return x;
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index e3f67044af3..496a8f1ac4c 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -973,9 +973,15 @@
int max(int i, int j)
{
+ /* Locals: tmp */
int tmp;
-
- if (i >= j) tmp = i; else tmp = j;
+ ;
+ if (i >= j) {
+ tmp = i;
+ }
+ else {
+ tmp = j;
+ }
return tmp;
}
[kernel:file:annotation] Marking properties
--
GitLab