From dca7c755d56c311798847ff7c57ec4e75115075a Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 27 Jul 2023 15:30:47 +0200
Subject: [PATCH] Update vis_spec script to also check fundec.sspec
---
tests/misc/oracle/vis_spec.res.oracle | 27 ++++++++++++++++++++++-----
tests/misc/vis_spec.ml | 27 ++++++++++++++++++---------
2 files changed, 40 insertions(+), 14 deletions(-)
diff --git a/tests/misc/oracle/vis_spec.res.oracle b/tests/misc/oracle/vis_spec.res.oracle
index ffe4ed60537..8151d594e44 100644
--- a/tests/misc/oracle/vis_spec.res.oracle
+++ b/tests/misc/oracle/vis_spec.res.oracle
@@ -1,8 +1,25 @@
[kernel] Parsing vis_spec.i (no preprocessing)
Starting visit
-Considering spec of function g
-Function prototype; Funspec is 'assigns \nothing;'
-Considering spec of function f
-Funspec of f is 'assigns \nothing;' through visitor
-It is 'assigns \nothing;' through get_spec
+Considering vspec of function g
+Function prototype; Funspec is
+'terminates \true;
+ exits \false;
+ allocates \nothing;'
+Considering sspec of function f
+Funspec of f is '' through visitor
+It is 'terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing;'
+through get_spec
+Considering vspec of function f
+Funspec of f is 'terminates \true;
+ exits \false;
+ allocates \nothing;'
+through visitor
+It is 'terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing;'
+through get_spec
End visit
diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml
index dce3f9c206d..19a8ae65685 100644
--- a/tests/misc/vis_spec.ml
+++ b/tests/misc/vis_spec.ml
@@ -5,18 +5,27 @@ class pathcrawlerVisitor prj =
object(self)
inherit Visitor.frama_c_copy prj
+ method! vfunc fundec =
+ Format.printf "Considering sspec of function %s@." fundec.svar.vname;
+ Format.printf "@[Funspec of %s is@ @['%a'@]@ through visitor@]@."
+ fundec.svar.vname
+ Printer.pp_funspec fundec.sspec;
+ Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
+ Printer.pp_funspec
+ (Annotations.funspec (Globals.Functions.get fundec.svar));
+ DoChildren
+
method! vspec sp =
- Format.printf "Considering spec of function %s@."
+ Format.printf "Considering vspec of function %s@."
(Kernel_function.get_name (Option.get self#current_kf));
(match self#current_func with
- | Some f ->
- if f.svar.vname ="f" then (
- Format.printf "@[Funspec of f is@ @['%a'@]@ through visitor@]@."
- Printer.pp_funspec sp;
- Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
- Printer.pp_funspec
- (Annotations.funspec (Globals.Functions.get f.svar));
- )
+ | Some fundec ->
+ Format.printf "@[Funspec of %s is@ @['%a'@]@ through visitor@]@."
+ fundec.svar.vname
+ Printer.pp_funspec sp;
+ Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
+ Printer.pp_funspec
+ (Annotations.funspec (Globals.Functions.get fundec.svar));
| None ->
Format.printf "@[Function prototype;@ Funspec is@ @['%a'@]@]@."
Printer.pp_funspec sp;
--
GitLab