[Obfuscate] avoid crash when modifying global lemmas

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)

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); */

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));
+
+*/