[obfuscate] Obfuscates axiomatics and lemmas

Since we modify the AST anyways, there's no reason to leave these names unchanged.

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
 

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/oracle/obfuscate.res.oracle

@@ -2,12 +2,12 @@
 [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 */
 /* *********************************** */
+// axiomatics
+#define A1 A
+#define A2 A1
 // behaviors
 #define B1 bhv
 // enums
@@ -31,6 +31,8 @@
 // logic constructors
 #define LC1 T
 #define LC2 F
+// lemmas
+#define LE1 OK
 // logic types
 #define LT1 t
 // logic variables
@@ -172,12 +174,12 @@ void F6(struct T2 *f6)
   return;
 }
 
-/*@ axiomatic A {
+/*@ axiomatic A1 {
       predicate LV3(void (*LV4)()) ;
       
       }
  */
-/*@ axiomatic A1 {
+/*@ axiomatic A2 {
       predicate LV5(void (*LV6)()) ;
       
       }
@@ -188,7 +190,7 @@ void F7(void)
   return;
 }
 
-/*@ lemma OK{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
+/*@ lemma LE1{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
 
 */