Skip to content

Commit 4d2b065

Browse files
committed
Fixed the struct test.desc
1 parent 15cf198 commit 4d2b065

File tree

2 files changed

+16
-9
lines changed
  • regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct

2 files changed

+16
-9
lines changed

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct/main.c

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,9 @@ void param_function(struct human a_human)
1111
__CPROVER_assert(a_human.height==1.80, "a_human.height==1.80");
1212
}
1313

14-
void param_function_mod(struct human *a_human)
14+
void param_function_val(struct human *a_human, int val)
1515
{
16-
a_human->age = 10;
17-
__CPROVER_assert(a_human->age==10, "a_human.age==10");
16+
a_human->age = val;
1817
}
1918

2019

@@ -25,11 +24,16 @@ void pass_param()
2524
human_instance.height = 1.80f;
2625
__CPROVER_assert(human_instance.age==24, "human_instance.age==24");
2726
__CPROVER_assert(human_instance.height==1.80f, "human_instance.height==1.80");
28-
param_function_mod(&human_instance);
27+
param_function_val(&human_instance, 10);
2928

3029
__CPROVER_assert(human_instance.age==10, "human_instance.age==10");
3130
__CPROVER_assert(human_instance.age==24, "human_instance.age==24");
3231
__CPROVER_assert(human_instance.height==1.80f, "human_instance.height==1.80");
32+
33+
param_function_val(&human_instance, 32);
34+
__CPROVER_assert(human_instance.age==32, "human_instance.age==32");
35+
__CPROVER_assert(human_instance.age==10, "human_instance.age==10");
36+
__CPROVER_assert(human_instance.height==1.80f, "human_instance.height==1.80");
3337
}
3438

3539
void global_struct_test()

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct/test.desc

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,12 @@ main.c
33
--function pass_param --variable --pointers --arrays --structs --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[pass_param.assertion.1\] file main.c line 26 function pass_param, human_instance.age==24: Success$
7-
^\[pass_param.assertion.2\] file main.c line 27 function pass_param, human_instance.height==1.80: Success$
8-
^\[pass_param.assertion.3\] file main.c line 30 function pass_param, human_instance.age==10: Success$
9-
^\[pass_param.assertion.4\] file main.c line 31 function pass_param, human_instance.age==24: Failure \(if reachable\)$
10-
^\[pass_param.assertion.5\] file main.c line 32 function pass_param, human_instance.height==1.80: Success$
6+
^\[pass_param.assertion.1\] .* human_instance.age==24: Success$
7+
^\[pass_param.assertion.2\] .* human_instance.height==1.80: Success$
8+
^\[pass_param.assertion.3\] .* human_instance.age==10: Success$
9+
^\[pass_param.assertion.4\] .* human_instance.age==24: Failure \(if reachable\)$
10+
^\[pass_param.assertion.5\] .* human_instance.height==1.80: Success$
11+
^\[pass_param.assertion.6\] .* human_instance.age==32: Unknown$
12+
^\[pass_param.assertion.7\] .* human_instance.age==10: Unknown$
13+
^\[pass_param.assertion.8\] .* human_instance.height==1.80: Success$
1114
--

0 commit comments

Comments
 (0)