Skip to content

Commit 3b16eb9

Browse files
committed
Add test for fixing of referencing of static symbols in harness file.
1 parent 3b2494f commit 3b16eb9

File tree

4 files changed

+35
-0
lines changed

4 files changed

+35
-0
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include "first_one.h"
2+
#include <assert.h>
3+
4+
static int static_function(int a)
5+
{
6+
assert(a == 0);
7+
return a;
8+
}
9+
10+
int non_static_function(int a)
11+
{
12+
return static_function(a);
13+
}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int non_static_function(int a);
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#include "first_one.h"
2+
3+
int another(int (*fun_ptr)(int), int c)
4+
{
5+
int a = (*fun_ptr)(c);
6+
7+
return a;
8+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
dummy.c
3+
--function another --harness-type call-function
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[static_function\.assertion\.1\] line \d assertion a == 0: FAILURE
7+
^VERIFICATION FAILED$
8+
--
9+
^CONVERSION ERROR$
10+
--
11+
For this particular error, we care mostly that goto-harness
12+
doesn't reference static symbols in other files, which would
13+
cause analysis through CBMC to fail with a conversion error.

0 commit comments

Comments
 (0)