Skip to content
Snippets Groups Projects

improve performance

Merged Andre Maroneze requested to merge improve-performance into master
Files
6
@@ -23017,28 +23017,71 @@ diff --git a/C/testcasesupport/std_testcase.h b/C/testcasesupport/std_testcase.h
index ef72327..5221d5e 100644
--- a/C/testcasesupport/std_testcase.h
+++ b/C/testcasesupport/std_testcase.h
@@ -80,6 +80,8 @@ class OneIntClass
@@ -33,6 +33,7 @@
# define __STDC_LIMIT_MACROS 1
#define ALLOCA alloca
+#include <alloca.h>
#endif
#include <stdio.h>
@@ -58,14 +59,14 @@
#include <new> // for placement new
/* classes used in some test cases as a custom type */
-class TwoIntsClass
+class TwoIntsClass
{
public: // Needed to access variables from label files
int intOne;
int intTwo;
};
-class OneIntClass
+class OneIntClass
{
public: // Needed to access variables from label files
int intOne;
@@ -80,17 +81,24 @@
#endif /* end ifndef __cplusplus */
+// RAND* definitions removed to avoid overflow-related UB in Frama-C
+#ifndef __FRAMAC__
/* rand only returns 15 bits, so we xor 3 calls together to get the full result (13 bits overflow, but that is okay) */
-/* rand only returns 15 bits, so we xor 3 calls together to get the full result (13 bits overflow, but that is okay) */
-// shifting signed values might overflow and be undefined
-#define URAND31() (((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand())
+
+// RAND* macros, adapted for Frama-C usage without UBs due to overflow
+#define URAND31() (((unsigned)(rand()%2)<<30) ^ ((unsigned)rand()<<15) ^ rand())
// choose to produce a positive or a negative number. Note: conditional only evaluates one URAND31
-#define RAND32() ((int)(rand() & 1 ? URAND31() : -URAND31() - 1))
+#define RAND32() (rand() & 1 ? (int)URAND31() : -(int)URAND31() - 1)
/* rand only returns 15 bits, so we xor 5 calls together to get the full result (11 bits overflow, but that is okay) */
// shifting signed values might overflow and be undefined
#define URAND31() (((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand())
@@ -92,6 +94,12 @@ class OneIntClass
-#define URAND63() (((uint64_t)rand()<<60) ^ ((uint64_t)rand()<<45) ^ ((uint64_t)rand()<<30) ^ ((uint64_t)rand()<<15) ^ rand())
+#define URAND63() (((uint64_t)(rand()%8)<<60) ^ ((uint64_t)rand()<<45) ^ ((uint64_t)rand()<<30) ^ ((uint64_t)rand()<<15) ^ rand())
// choose to produce a positive or a negative number. Note: conditional only evaluates one URAND63
#define RAND64() ((int64_t)(rand() & 1 ? URAND63() : -URAND63() - 1))
+// Frama-C defines the macros below differently
+#define RAND16(x) RAND32(x)
+#define RAND8(x) RAND32(x)
-#define RAND64() ((int64_t)(rand() & 1 ? URAND63() : -URAND63() - 1))
+#define RAND64() (rand() & 1 ? (int64_t)URAND63() : -(int64_t)URAND63() - 1)
+
+#endif
+// Extra definitions to avoid downcasts in some tests
+#define URAND15() (rand() % (1<<15))
+#define RAND16() (rand() & 1 ? (short)URAND15() : -((short)URAND15()) - 1)
+
+#define URAND7() (rand() % (1<<7))
+#define RAND8() (rand() & 1 ? (char)URAND7() : -((char)URAND7()) - 1)
/* struct used in some test cases as a custom type */
typedef struct _twoIntsStruct
{
--
@@ -104,8 +112,7 @@
#endif
/* The variables below are declared "const", so a tool should
- be able to identify that reads of these will always return their
+ be able to identify that reads of these will always return their
initialized values. */
extern const int GLOBAL_CONST_TRUE; /* true */
extern const int GLOBAL_CONST_FALSE; /* false */
--
2.9.5
Loading