From d3dc9f6d4c25ac83acd1639cb2df0bb195d1924b Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@kit.edu>
Date: Mon, 6 Jul 2020 16:24:08 +0200
Subject: [PATCH] Add test and oracle for supported recursive extended global
annotations
---
tests/spec/Extend_recursive_preprocess.i | 31 +------------
tests/spec/Extend_recursive_preprocess.ml | 43 +++++++++++++++++++
.../Extend_recursive_preprocess.res.oracle | 20 +++++++++
3 files changed, 65 insertions(+), 29 deletions(-)
create mode 100644 tests/spec/Extend_recursive_preprocess.ml
create mode 100644 tests/spec/oracle/Extend_recursive_preprocess.res.oracle
diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
index ce540ac794c..6bd8a322856 100644
--- a/tests/spec/Extend_recursive_preprocess.i
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -3,33 +3,6 @@ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
*/
-/*@ bhv_foo must_replace(x); */
-int f(int x);
-
-/*@ behavior test:
- bhv_foo must_replace(x);
-*/
-int g(int x);
-
-
-int f(int x) {
- int s = 0;
- /*@ loop nl_foo must_replace(x); */
- for (int i = 0; i < x; i++) s+=g(i);
- /*@ ca_foo must_replace(x); */
- return s;
-}
-
-int k(int z) {
- int x = z;
- int y = 0;
- /*@ ns_foo must_replace(x); */
- y = x++;
- return y;
-}
-
-/*@ gl_foo must_replace(x); */
-
/*@ gl_foo foo1 {
gl_fooo must_replace(x);
@@ -38,9 +11,9 @@ int k(int z) {
gl_foo foo3 {
gl_fooo must_replace(x);
gl_fooo must_replace(x);
- };
+ }
gl_fooo must_replace(x);
- };
+ }
gl_fooo must_replace(x);
}*/
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
new file mode 100644
index 00000000000..528d53057bf
--- /dev/null
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -0,0 +1,43 @@
+open Logic_ptree
+open Logic_const
+
+let validate call =
+ assert (not (String.equal "must_replace" call)) ;
+ match String.split_on_char '_' call with
+ | [ lkind ; lok ] -> String.equal "gl_fooo" lkind && String.equal lok "ok"
+ | _ -> false
+
+let ext_typing_fooo _typing_context _loc l =
+ let type_lexpr = function
+ | { lexpr_node = PLapp(s, [], [ _ ]) } when validate s -> ptrue
+ | _ -> pfalse
+ in
+ Cil_types.Ext_preds (List.map type_lexpr l)
+
+let ext_typing_block typing_context loc_here node =
+ match node.extended_node with
+ | Ext_lexpr (name,data) ->
+ let status,kind = Logic_typing.get_typer name typing_context node.extended_loc data in
+ Logic_const.new_acsl_extension name loc_here status kind
+ | Ext_extension (name, id, data) ->
+ let status,kind = Logic_typing.get_typer_block name typing_context node.extended_loc (id,data) in
+ Logic_const.new_acsl_extension name loc_here status kind
+
+let ext_typing_foo typing_context loc (s,d) =
+ let block = List.map (ext_typing_block typing_context loc) d in
+ Cil_types.Ext_annot (s,block)
+
+let preprocess_fooo_ptree_element = function
+ | { lexpr_node = PLapp("must_replace", [], [ v ]) } as x ->
+ { x with lexpr_node = PLapp("gl_foo" ^ "_ok", [], [ v ]) }
+ | x -> x
+
+let preprocess_fooo_ptree = List.map preprocess_fooo_ptree_element
+
+let preprocess_foo_ptree (id,data) =(id ^ "_ok",data)
+
+let () =
+ Acsl_extension.register_global
+ "gl_fooo" ~preprocessor:preprocess_fooo_ptree ext_typing_fooo false ;
+ Acsl_extension.register_global_block
+ "gl_foo" ~preprocessor:preprocess_foo_ptree ext_typing_foo false
diff --git a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
new file mode 100644
index 00000000000..ec48b5138f4
--- /dev/null
+++ b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/spec/Extend_recursive_preprocess.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+gl_foo foo1_ok {
+ gl_fooo \false;
+ gl_foo foo2_ok {
+ gl_fooo \false;
+ gl_foo foo3_ok {
+ gl_fooo \false;
+ gl_fooo \false;
+ }
+ ;
+ gl_fooo \false;
+ }
+ ;
+ gl_fooo \false;
+ }
+ ;
+*/
+
--
GitLab