improve performance

fc/patches/improve-testcasesupport.patch

@@ -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