From b2c174b569dedc3adaa6213af437eadf384270c1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 25 Nov 2021 09:16:14 +0100
Subject: [PATCH] [Obfuscate] avoid crash when modifying global lemmas

---
 src/plugins/obfuscator/obfuscate.ml    |  2 +-
 tests/misc/obfuscate.c                 |  6 ++++++
 tests/misc/oracle/obfuscate.res.oracle | 27 ++++++++++++++++++++++++++
 3 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 29ac575f135..3decde3ce5c 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -290,7 +290,7 @@ end
 let obfuscate () =
   Dictionary.mark_as_computed ();
   obfuscate_behaviors ();
-  Visitor.visitFramacFileSameGlobals
+  Visitor.visitFramacFile
     (new visitor :> Visitor.frama_c_visitor)
     (Ast.get ());
   Printer.update_printer (module UpdatePrinter: Printer.PrinterExtension)
diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c
index 0fb0323afb8..34a705ecd97 100644
--- a/tests/misc/obfuscate.c
+++ b/tests/misc/obfuscate.c
@@ -72,3 +72,9 @@ void implem(int c, int d) { };
 struct S example_struct = { .my_func = implem };
 
 void test_func(struct S* s) { s->my_func(3,4); example_struct.my_func(5,6); }
+
+// Check that these definitions do not make obfuscate crash
+/*@ axiomatic A { predicate P(void (*galois_fp_old)()); } */
+/*@ axiomatic A1 { predicate P1(void (*galois_fp_old)()); } */
+void my_f() {}
+/*@ lemma OK: P(my_f) && P1(my_f); */
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index 124447020ca..e36f5683039 100644
--- a/tests/misc/oracle/obfuscate.res.oracle
+++ b/tests/misc/oracle/obfuscate.res.oracle
@@ -2,6 +2,9 @@
 [obfuscator] Warning: unobfuscated attribute name `fc_stdlib'
 [obfuscator] Warning: unobfuscated attribute parameter name `stdint.h'
 [obfuscator] Warning: unobfuscated attribute name `missingproto'
+[obfuscator] Warning: unobfuscated axiomatic name `A'
+[obfuscator] Warning: unobfuscated axiomatic name `A1'
+[obfuscator] Warning: unobfuscated lemma name `OK'
 /* *********************************** */
 /* start of dictionary for obfuscation */
 /* *********************************** */
@@ -18,6 +21,7 @@
 #define F4 builtin_and_stdlib
 #define F5 implem
 #define F6 test_func
+#define F7 my_f
 // global variables
 #define G1 my_var
 #define G2 example_struct
@@ -32,6 +36,10 @@
 // logic variables
 #define LV1 I
 #define LV2 x
+#define LV3 P
+#define LV4 galois_fp_old
+#define LV5 P1
+#define LV6 galois_fp_old
 // fields
 #define M1 my_func
 // predicates
@@ -164,4 +172,23 @@ void F6(struct T2 *f6)
   return;
 }
 
+/*@ axiomatic A {
+      predicate LV3(void (*LV4)()) ;
+      
+      }
+ */
+/*@ axiomatic A1 {
+      predicate LV5(void (*LV6)()) ;
+      
+      }
+
+*/
+void F7(void)
+{
+  return;
+}
+
+/*@ lemma OK{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
+
+*/
 
-- 
GitLab