From 63fa5407d58fc12865e572adb2bd3e60e6c45d0b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Mon, 26 Nov 2018 10:16:01 +0100
Subject: [PATCH] [Kernel/test] Cil.changeTo instruction list in ghost
---
tests/cil/change_to_instr.i | 17 ++++++++++++++
tests/cil/change_to_instr.ml | 17 ++++++++++++++
tests/cil/oracle/change_to_instr.res.oracle | 25 +++++++++++++++++++++
3 files changed, 59 insertions(+)
create mode 100644 tests/cil/change_to_instr.i
create mode 100644 tests/cil/change_to_instr.ml
create mode 100644 tests/cil/oracle/change_to_instr.res.oracle
diff --git a/tests/cil/change_to_instr.i b/tests/cil/change_to_instr.i
new file mode 100644
index 00000000000..b83b32608f6
--- /dev/null
+++ b/tests/cil/change_to_instr.i
@@ -0,0 +1,17 @@
+/* run.config
+OPT: -load-script tests/cil/change_to_instr.ml -print
+*/
+
+
+int main(){
+ int i = 0 ;
+ //@ ghost int j = 0 ;
+
+ i++ ;
+ //@ ghost j++ ;
+
+ {
+ //@ ghost int x = 0;
+ //@ ghost x++ ;
+ }
+}
diff --git a/tests/cil/change_to_instr.ml b/tests/cil/change_to_instr.ml
new file mode 100644
index 00000000000..04d2679952d
--- /dev/null
+++ b/tests/cil/change_to_instr.ml
@@ -0,0 +1,17 @@
+class add_skip = object(_)
+ inherit Visitor.frama_c_inplace
+
+ method! vfunc f =
+ File.must_recompute_cfg f ;
+ Cil.DoChildren
+
+ method! vinst i =
+ let open Cil_types in
+ Cil.ChangeTo [ Skip(Cil.CurrentLoc.get()) ; i ]
+end
+
+let run () =
+ Visitor.visitFramacFileSameGlobals (new add_skip) (Ast.get())
+
+let () =
+ Db.Main.extend run
diff --git a/tests/cil/oracle/change_to_instr.res.oracle b/tests/cil/oracle/change_to_instr.res.oracle
new file mode 100644
index 00000000000..590858bb9f0
--- /dev/null
+++ b/tests/cil/oracle/change_to_instr.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing tests/cil/change_to_instr.i (no preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ ;
+ int i = 0;
+ /*@ ghost ; */
+ /*@ ghost int j = 0; */
+ ;
+ i ++;
+ /*@ ghost ; */
+ /*@ ghost j ++; */
+ {
+ /*@ ghost ; */
+ /*@ ghost int x = 0; */
+ /*@ ghost ; */
+ /*@ ghost x ++; */
+ }
+ ;
+ __retres = 0;
+ return __retres;
+}
+
+
--
GitLab