Merge branch 'fix/andre/obfuscate-crash' into 'master'

[Obfuscate] avoid crash when modifying global lemmas

See merge request frama-c/frama-c!3465

src/plugins/obfuscator/obfuscate.ml

@@ -166,12 +166,13 @@ class visitor = object
     Cil.DoChildren
 
   method! vannotation = function
-    | Daxiomatic(str, _, _, _) ->
-      warn "axiomatic" str;
-      Cil.DoChildren
-    | Dlemma(str, _, _, { tp_kind }, _, _) ->
-      warn (Cil_printer.string_of_lemma tp_kind) str;
-      Cil.DoChildren
+    | Daxiomatic(str, globs, attrs, loc) ->
+      let str' = Dictionary.fresh Obfuscator_kind.Axiomatic str in
+      Cil.ChangeDoChildrenPost(Daxiomatic(str',globs,attrs,loc),Extlib.id)
+    | Dlemma(str, labs, typs, pred, attrs, loc) ->
+      let str' = Dictionary.fresh Obfuscator_kind.Lemma str in
+      Cil.ChangeDoChildrenPost(
+        Dlemma(str',labs,typs, pred, attrs, loc),Extlib.id)
     | _ ->
       Cil.DoChildren
 
@@ -290,7 +291,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)

src/plugins/obfuscator/obfuscator_kind.ml

@@ -36,6 +36,8 @@ type k =
   | Type
   | Logic_type
   | Logic_constructor
+  | Axiomatic
+  | Lemma
 
 let name_of_kind = function
   | Behavior -> "behavior"
@@ -53,6 +55,8 @@ let name_of_kind = function
   | Type -> "type"
   | Logic_type -> "logic type"
   | Logic_constructor -> "logic constructor"
+  | Axiomatic -> "axiomatic"
+  | Lemma -> "lemma"
 
 let prefix = function
   | Behavior -> "B"
@@ -70,6 +74,8 @@ let prefix = function
   | Type -> "T"
   | Logic_type -> "LT"
   | Logic_constructor -> "LC"
+  | Axiomatic -> "A"
+  | Lemma -> "LE"
 
 include Datatype.Make_with_collections
     (struct

src/plugins/obfuscator/obfuscator_kind.mli

@@ -36,6 +36,8 @@ type k =
   | Type
   | Logic_type
   | Logic_constructor
+  | Axiomatic
+  | Lemma
 
 include Datatype.S_with_collections with type t = k
 val prefix: t -> string

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

@@ -5,6 +5,9 @@
 /* *********************************** */
 /* start of dictionary for obfuscation */
 /* *********************************** */
+// axiomatics
+#define A1 A
+#define A2 A1
 // behaviors
 #define B1 bhv
 // enums
@@ -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
@@ -27,11 +31,17 @@
 // logic constructors
 #define LC1 T
 #define LC2 F
+// lemmas
+#define LE1 OK
 // logic types
 #define LT1 t
 // 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 +174,23 @@ void F6(struct T2 *f6)
   return;
 }
 
+/*@ axiomatic A1 {
+      predicate LV3(void (*LV4)()) ;
+      
+      }
+ */
+/*@ axiomatic A2 {
+      predicate LV5(void (*LV6)()) ;
+      
+      }
+
+*/
+void F7(void)
+{
+  return;
+}
+
+/*@ lemma LE1{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
+
+*/