[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 */
/* *********************************** */
// behaviors
#define B1 bhv
// enums
#define E1 first
#define E2 second
#define E3 third
// functions
#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
// predicates
#define P1 never
// types
#define T1 my_enum
// local variables
#define V1 x
#define V2 __retres
#define V3 V1
#define V4 __retres
#define V5 x
#define V6 __retres
// formal variables
#define f1 p
#define f2 f1
#define f3 p
/*********************************** */
/* end of dictionary for obfuscation */
/*********************************** */

/* *********************************************************** */
/* start of dictionary required to compile the obfuscated code */
/* *********************************************************** */
// literal strings
#define LS1 "ti\rti"
/* ********************************************************* */
/* end of dictionary required to compile the obfuscated code */
/* ********************************************************* */

/* Generated by Frama-C */
#include "stdint.h"
enum T1 {
    E1 = 0,
    E2 = 1,
    E3 = 4
};
int G1 = 0;
/*@ global invariant LV1: G1 ≥ 0;

*/
/*@ requires G1 > 0;
    ensures G1 > \old(G1);
    ensures ∀ ℤ LV2; LV2 ≡ LV2;
 */
int F1(void)
{
  int V2;
  enum T1 V1 = E1;
  /*@ assert G1 ≥ E1; */ ;
  G1 ++;
  if (! G1) goto L1;
  V2 = (int)((unsigned int)G1 + V1);
  goto return_label;
  L1: ;
  V2 = -1;
  return_label: return V2;
}

/*@ requires \valid(f1);
    ensures *\old(f1) ≡ 0; */
void F2(int *f1);

/*@ behavior B1:
      exits P1: \false;
    
    complete behaviors B1;
    disjoint behaviors B1;
 */
int F3(int f2)
{
  int V3;
  V3 = 0;
  if (f2) goto L2;
  V3 ++;
  /*@ assert property: V3 ≢ 0? 1 ≢ 0: 0 ≢ 0; */ ;
  L2: ;
  return V3;
}

int main(int *f3)
{
  int V4;
  if (LS1 == LS1) F2(f3);
  V4 = 0;
  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;
}