Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
sate-6
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Container Registry
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
sate-6
Merge requests
!1
improve performance
Code
Review changes
Check out branch
Download
Patches
Plain diff
Merged
improve performance
improve-performance
into
master
Overview
0
Commits
5
Pipelines
0
Changes
6
Merged
Andre Maroneze
requested to merge
improve-performance
into
master
3 years ago
Overview
0
Commits
5
Pipelines
0
Changes
6
Expand
0
0
Merge request reports
Compare
master
version 7
7e2475e5
3 years ago
version 6
de08e459
3 years ago
version 5
789f16dc
3 years ago
version 4
fb22a711
3 years ago
version 3
3030a9ee
3 years ago
version 2
f2b83d53
3 years ago
version 1
7d840003
3 years ago
master (base)
and
latest version
latest version
b74ea4a8
5 commits,
3 years ago
version 7
7e2475e5
5 commits,
3 years ago
version 6
de08e459
5 commits,
3 years ago
version 5
789f16dc
4 commits,
3 years ago
version 4
fb22a711
3 commits,
3 years ago
version 3
3030a9ee
3 commits,
3 years ago
version 2
f2b83d53
2 commits,
3 years ago
version 1
7d840003
1 commit,
3 years ago
6 files
+
154
−
72
Inline
Compare changes
Side-by-side
Inline
Show whitespace changes
Show one file at a time
Files
6
Search (e.g. *.vue) (Ctrl+P)
fc/patches/improve-testcasesupport.patch
+
57
−
14
Options
@@ -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 URAND3
1
() (((u
nsigned
)rand()<<30) ^ ((u
nsigned
)rand()<<15) ^ rand())
@@ -92,6 +94,12 @@ class OneIntClass
-
#define URAND
6
3() (((u
int64_t)rand()<<60) ^ ((uint64_t)rand()<<45) ^ ((uint64_t
)rand()<<30) ^ ((u
int64_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