-
Andre Maroneze authored
Some case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
Andre Maroneze authoredSome case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
obfuscate.res.oracle 2.00 KiB
[kernel] Parsing tests/misc/obfuscate.i (no preprocessing)
/* *********************************** */
/* 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
// global variables
#define G1 my_var
// labels
#define L1 end
#define L2 end
// 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
// 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 */
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;
}