From a1419d2aa149ef232ebe4f7c9c8ca79a9fb2c19c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 25 Feb 2019 15:46:03 +0100
Subject: [PATCH] [obfuscator] Adds some tests.

---
 tests/misc/{obfuscate.i => obfuscate.c} | 13 ++++++++++
 tests/misc/oracle/obfuscate.res.oracle  | 32 +++++++++++++++++++++++--
 2 files changed, 43 insertions(+), 2 deletions(-)
 rename tests/misc/{obfuscate.i => obfuscate.c} (73%)

diff --git a/tests/misc/obfuscate.i b/tests/misc/obfuscate.c
similarity index 73%
rename from tests/misc/obfuscate.i
rename to tests/misc/obfuscate.c
index 044b97cb3c9..ade70e66898 100644
--- a/tests/misc/obfuscate.i
+++ b/tests/misc/obfuscate.c
@@ -46,3 +46,16 @@ int logic(int f1)
 int main(int* p) { 
   if ("ti\rti" == "ti\rti") f(p); 
 }
+
+/* Obfuscate logic types and logic constructors. */
+/*@ type t = T | F; */
+
+#include "stdint.h"
+
+/* Do not obfuscate builtins and stdlib types and functions. */
+int builtin_and_stdlib () {
+  int32_t x = 42;
+  Frama_C_show_each(x);
+  /*@ assert \true; */
+  return 1;
+}
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index 6ba918f0252..efd7abd9fba 100644
--- a/tests/misc/oracle/obfuscate.res.oracle
+++ b/tests/misc/oracle/obfuscate.res.oracle
@@ -1,4 +1,7 @@
-[kernel] Parsing tests/misc/obfuscate.i (no preprocessing)
+[kernel] Parsing tests/misc/obfuscate.c (with preprocessing)
+[obfuscator] Warning: unobfuscated attribute name `fc_stdlib'
+[obfuscator] Warning: unobfuscated attribute parameter name `stdint.h'
+[obfuscator] Warning: unobfuscated attribute name `missingproto'
 /* *********************************** */
 /* start of dictionary for obfuscation */
 /* *********************************** */
@@ -12,11 +15,17 @@
 #define F1 my_func
 #define F2 f
 #define F3 logic
+#define F4 builtin_and_stdlib
 // global variables
 #define G1 my_var
 // labels
 #define L1 end
 #define L2 end
+// logic constructors
+#define LC1 T
+#define LC2 F
+// logic types
+#define LT1 t
 // logic variables
 #define LV1 I
 #define LV2 x
@@ -29,6 +38,8 @@
 #define V2 __retres
 #define V3 V1
 #define V4 __retres
+#define V5 x
+#define V6 __retres
 // formal variables
 #define f1 p
 #define f2 f1
@@ -47,6 +58,7 @@
 /* ********************************************************* */
 
 /* Generated by Frama-C */
+#include "stdint.h"
 enum T1 {
     E1 = 0,
     E2 = 1,
@@ -54,7 +66,8 @@ enum T1 {
 };
 int G1 = 0;
 /*@ global invariant LV1: G1 ≥ 0;
- */
+
+*/
 /*@ requires G1 > 0;
     ensures G1 > \old(G1);
     ensures ∀ ℤ LV2; LV2 ≡ LV2;
@@ -102,4 +115,19 @@ int main(int *f3)
   return V4;
 }
 
+/*@ type LT1 = LC1 | LC2;
+
+*/
+extern int ( /* missing proto */ Frama_C_show_each)();
+
+int F4(void)
+{
+  int V6;
+  int32_t V5 = 42;
+  Frama_C_show_each(V5);
+  /*@ assert \true; */ ;
+  V6 = 1;
+  return V6;
+}
+
 
-- 
GitLab